Homepage > Man Pages > Category > General Commands
Homepage > Man Pages > Name > G

gallina

man page of gallina

gallina: extracts specification from Coq vernacular files

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 GALLINA(1)
 
 
 

Copyright © 2011–2018 by topics-of-interest.com . All rights reserved. Hosted by all-inkl.
Contact · Imprint · Privacy

Page generated in 25.01ms.

daelim-forum.spreadshirt.de | dfptutorial.com | tier-bedarf.com