## 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