diff options
Diffstat (limited to 'man/gallina.1')
-rw-r--r-- | man/gallina.1 | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/man/gallina.1 b/man/gallina.1 new file mode 100644 index 00000000..8c607216 --- /dev/null +++ b/man/gallina.1 @@ -0,0 +1,74 @@ +.TH COQ 1 "29 March 1995" "Coq tools" + +.SH NAME +gallina \- extracts specification from Coq vernacular files + +.SH SYNOPSIS +.B gallina +[ +.BI \- +] +[ +.BI \-stdout +] +[ +.BI \-nocomments +] +.I file ... + +.SH DESCRIPTION + +.B gallina +takes Coq files as arguments and builds the corresponding +specification files. +The Coq file +.IR foo.v \& +gives bearth to the specification file +.IR 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" command. + +Files without the .v suffix are ignored. + + +.SH OPTIONS + +.TP +.BI \-stdout +Prints the result on standard output. +.TP +.BI \- +Coq source is taken on standard input. The result is printed on +standard output. +.TP +.BI \-nocomments +Comments are removed in the *.g file. + +.SH NOTES + +Nested comments are correctly handled. In particular, every command +"Save." or "Abort." in a comment is not taken into account. + + +.SH BUGS + +Please report any bug to +.B coq@pauillac.inria.fr + + + + + + + + + + + + + |