DragonFly On-Line Manual Pages

COQ(1)                 DragonFly 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
       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
       command "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)