This is the command gallina that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
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.
Use gallina online using onworks.net services
