1COQ(1)                      General Commands Manual                     COQ(1)
2
3
4

NAME

6       gallina - extracts specification from Coq vernacular files
7
8

SYNOPSIS

10       gallina [ - ] [ -stdout ] [ -nocomments ] file ...
11
12

DESCRIPTION

14       gallina takes Coq files as arguments and builds the corresponding spec‐
15       ification files.  The Coq file foo.v gives bearth to the  specification
16       file foo.g. The suffix '.g' stands for Gallina.
17
18       For that purpose, gallina removes all commands that follow a "Theorem",
19       "Lemma", "Fact", "Remark" or "Goal" statement until it reaches  a  com‐
20       mand  "Abort.",  "Save.", "Qed.", "Defined." or "Proof <...>.". It also
21       removes every "Hint", "Syntax", "Immediate"  or "Transparent" command.
22
23       Files without the .v suffix are ignored.
24
25
26

OPTIONS

28       -stdout
29              Prints the result on standard output.
30
31       -      Coq source is taken on standard input. The result is printed  on
32              standard output.
33
34       -nocomments
35              Comments are removed in the *.g file.
36
37

NOTES

39       Nested  comments  are  correctly  handled. In particular, every command
40       "Save." or "Abort." in a comment is not taken into account.
41
42
43

BUGS

45       Please report any bug to coq@pauillac.inria.fr
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62Coq tools                        29 March 1995                          COQ(1)