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

NAME

6       coqide - The Coq Proof Assistant graphical interface
7
8
9

SYNOPSIS

11       coqide [ options ]
12
13

DESCRIPTION

15       coqide is a gtk graphical interface for the Coq proof assistant.
16
17       For  command-line-oriented  use  of Coq, see coqtop(1) ; for batch-ori‐
18       ented use of Coq, see coqc(1).
19
20
21

OPTIONS

23       -h     Show the complete list of options accepted by coqide.
24
25       -I dir, -include dir
26              Add directory dir in the include path.
27
28       -R dir coqdir
29              Recursively map physical dir to logical coqdir.
30
31       -src   Add source directories in the include path.
32
33       -nois  Start with an empty state.
34
35       -load-ml-object f
36              Load ML object file f.
37
38       -load-ml-source f
39              Load ML file f.
40
41       -l f, -load-vernac-source f
42              Load Coq file f.v (Load f.).
43
44       -lv f, -load-vernac-source-verbose f
45              Load Coq file f.v (Load Verbose f.).
46
47       -load-vernac-object path
48              Load Coq library path (Require path.).
49
50       -require path
51              Load Coq library path and import it (Require Import path.).
52
53       -compile f
54              Compile Coq file f.v (implies -batch).
55
56       -compile-verbose f
57              Verbosely compile Coq file f.v (implies -batch).
58
59       -where Print Coq's standard library location and exit.
60
61       -v     Print Coq version and exit.
62
63       -q     Skip loading of rcfile.
64
65       -init-file f
66              Set the rcfile to f.
67
68       -batch Batch mode (exits just after arguments parsing).
69
70       -boot  Boot mode (implies -q and -batch).
71
72       -emacs Tells Coq it is executed under Emacs.
73
74       -dump-glob f
75              Dump globalizations in file f (to be used by coqdoc(1)).
76
77       -impredicative-set
78              Set sort Set impredicative.
79
80       -dont-load-proofs
81              Don't load opaque proofs in memory.
82
83       -xml   Export XML files either to the hierarchy rooted in the directory
84              COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).
85
86
87

SEE ALSO

89       coqc(1), coqtop(1), coq-tex(1), coqdep(1).
90       The  Coq  Reference  Manual,  The  Coq  web  site: http://coq.inria.fr,
91       /usr/share/doc/coqide/FAQ.
92
93

AUTHOR

95       This manual page  was  written  by  Samuel  Mimram  <samuel.mimram@ens-
96       lyon.org>, for the Debian project (but may be used by others).
97
98
99
100                                 July 16, 2004                       COQIDE(1)
Impressum