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)
