The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

In his message of Wed February 3, 1999, Randy Pollack writes: 
> What is the intended use of ".g" files created from ".v" files by the
> "gallina" command?

The gallina file .g is just the version of the vernacular file .v without
the proofs. Thus, you have the whole development (definitions, syntax,
lemmas, etc.) but without the hundreds lines of proof.

It is useful when you want to document a Coq development, and in
particular as a first pass before coq2html or coq2latex (as for
instance in the documentation of the Coq standard library).

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr