1COQ(1) General Commands Manual COQ(1)
2
3
4
6 coqtop - The Coq Proof Assistant toplevel system
7
8
9
11 coqtop [ options ]
12
13
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
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 (resource file) if any
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 -impredicative-set
103 set sort Set impredicative
104
105
106 -dont-load-proofs
107 don't load opaque proofs in memory
108
109
111 coqc(1), coq-tex(1), coqdep(1).
112 The Coq Reference Manual. The Coq web site: http://coq.inria.fr
113
114
115
116 October 11, 2006 COQ(1)