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

NAME

6       coqtop - The Coq Proof Assistant toplevel system
7
8
9

SYNOPSIS

11       coqtop [ options ]
12
13

DESCRIPTION

15       coqtop  is  the  toplevel system of Coq, for interactive use.  It reads
16       phrases on the standard input, and prints results on the standard  out‐
17       put.
18
19       For batch-oriented use of Coq, see coqc(1).
20
21
22

OPTIONS

24       -h, --help
25              Help.  Will  give  you  the complete list of options accepted by
26              coqtop.
27
28
29       -I dir, --include dir
30              add directory dir in the include path
31
32
33       -R dir coqdir
34              recursively map physical dir to logical coqdir
35
36
37       -top coqdir
38              set the toplevel name to be coqdir instead of Top
39
40
41       -inputstate filename, -is filename
42              read state from file filename.coq
43
44
45       -nois  start with an empty intial state
46
47
48       -outputstatefilename
49              write state in file filename.coq
50
51
52       -load-ml-object filename
53              load ML object file filenname
54
55
56       -load-ml-source filename
57              load ML file filename
58
59
60       -load-vernac-source filename, -l filename
61              load Coq file filename.v (Load filename.)
62
63
64       -load-vernac-source-verbose filename, -lv filename
65              load verbosely Coq file filename.v (Load Verbose filename.)
66
67
68       -load-vernac-object filename
69              load Coq object file filename.vo
70
71
72       -require filename
73              load Coq object file filename.vo and import it  (Require  Import
74              filename.)
75
76
77       -compile filename
78              compile Coq file filename.v (implies -batch )
79
80
81       -compile-verbose filename
82              verbosely compile Coq file filename.v (implies -batch )
83
84
85       -opt   run the native-code version of Coq
86
87
88       -byte  run the bytecode version of Coq
89
90
91       -where print Coq's standard library location and exit
92
93
94       -v     print Coq version and exit
95
96
97       -q     skip loading of rcfile
98
99
100       -init-file filename
101              set the rcfile to filename
102
103
104       -user uid
105              use the rcfile of user uid
106
107
108
109       -batch batch mode (exits just after arguments parsing)
110
111
112       -boot  boot mode (implies -q and -batch )
113
114
115       -emacs tells Coq it is executed under Emacs
116
117
118       -dump-glob filename
119              dump globalizations in file f (to be used by coqdoc(1) )
120
121
122       -with-geoproof (yes|no)
123              to  (de)activate  special  functions  for Geoproof within Coqide
124              (default is yes )
125
126
127       -impredicative-set
128              set sort Set impredicative
129
130
131       -dont-load-proofs
132              don't load opaque proofs in memory
133
134
135       -xml   export XML files either to the hierarchy rooted in the directory
136              $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)
137
138
139       -quality
140              improve  the legibility of the proof terms produced by some tac‐
141              tics
142
143

SEE ALSO

145       coqc(1), coq-tex(1), coqdep(1).
146       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
147
148
149
150                               October 11, 2006                         COQ(1)
Impressum