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