COQ(1)COQ(1)NAMEgallina - extracts specification from Coq vernacular files
SYNOPSISgallina [ - ] [ -stdout ] [ -nocomments ] file ...
DESCRIPTIONgallina takes Coq files as arguments and builds the corresponding spec‐
ification files. The Coq file foo.v gives bearth to the specification
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 com‐
mand "Abort.", "Save.", "Qed.", "Defined." or "Proof <...>.". It also
removes every "Hint", "Syntax", "Immediate" or "Transparent" command.
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)