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       -nois  start with an empty initial state
42
43
44       -load-ml-object filename
45              load ML object file filenname
46
47
48       -load-ml-source filename
49              load ML file filename
50
51
52       -load-vernac-source filename, -l filename
53              load Coq file filename.v (Load filename.)
54
55
56       -load-vernac-source-verbose filename, -lv filename
57              load verbosely Coq file filename.v (Load Verbose filename.)
58
59
60       -load-vernac-object path
61              load Coq library path (Require path.)
62
63
64       -require path
65              load Coq library path and import it (Require Import path.)
66
67
68       -compile filename.v
69              compile Coq file filename.v (implies -batch )
70
71
72       -compile-verbose filename.v
73              verbosely compile Coq file filename.v (implies -batch )
74
75
76       -where print Coq's standard library location and exit
77
78
79       -v     print Coq version and exit
80
81
82       -q     skip loading of rcfile
83
84
85       -init-file filename
86              set the rcfile to filename
87
88
89       -batch batch mode (exits just after arguments parsing)
90
91
92       -boot  boot mode (implies -q and -batch )
93
94
95       -emacs tells Coq it is executed under Emacs
96
97
98       -dump-glob filename
99              dump globalizations in file f (to be used by coqdoc(1) )
100
101
102       -with-geoproof (yes|no)
103              to (de)activate special functions  for  Geoproof  within  Coqide
104              (default is yes )
105
106
107       -impredicative-set
108              set sort Set impredicative
109
110
111       -dont-load-proofs
112              don't load opaque proofs in memory
113
114
115       -xml   export XML files either to the hierarchy rooted in the directory
116              $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)
117
118

SEE ALSO

120       coqc(1), coq-tex(1), coqdep(1).
121       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
122
123
124
125                               October 11, 2006                         COQ(1)
Impressum