gistfile1.txt

*
*	gallina		May 20 1994 (Jean-Christophe Filliatre)
*

SYNOPSIS

	gallina [-] [-stdout] file1 file2 ...

DESCRIPTION

	gallina takes a Coq file (foo.v) and builds the corresponding
	specification file (foo.g). '.g' stands for Gallina.

	For that purpose, gallina removes all commands that follow
	"Theorem <...>.", "Lemma <...>." or "Remark <...>." until
	it reaches a command "Abort.", "Save." or "Proof <...>.",
	and every command "Hint ...", "Syntax ...", "Immediate ..."
	or "Transparent ...".

	One can give a list of files as argument. 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 given on
	standard output.
		
CHARACTERISTICS

	The (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