debian man page for gallina

COQ(1)							      General Commands Manual							    COQ(1)

NAME
       gallina - extracts specification from Coq vernacular files

SYNOPSIS
       gallina [ - ] [ -stdout ] [ -nocomments ] file ...

DESCRIPTION
       gallina	takes  Coq files as arguments and builds the corresponding specification files.  The Coq file foo.v gives bearth to the specifica-
       tion file foo.g. The suffix '.g' stands for Gallina.

       For that purpose, gallina removes all commands that follow a "Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until  it	reaches  a
       command "Abort.", "Save.", "Qed.", "Defined." or "Proof <...>.". It also removes every "Hint", "Syntax", "Immediate"  or "Transparent" com-
       mand.

       Files without the .v suffix are ignored.

OPTIONS
       -stdout
	      Prints the result on standard output.

       -      Coq source is taken on standard input. The result is printed on standard output.

       -nocomments
	      Comments are removed in the *.g file.

NOTES
       Nested comments are correctly handled. In particular, every command "Save." or "Abort." in a comment is not taken into account.

BUGS
       Please report any bug to coq@pauillac.inria.fr

Coq tools							   29 March 1995							    COQ(1)