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       coqtop is a gtk graphical interface for the Coq proof assistant.
16
17       For  command-line-oriented  use  of Coq, see coqide(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       -is f, -inputstate f
34              Read state from f.coq.
35
36       -nois  Start with an empty state.
37
38       -outputstate f
39              Write state in file f.coq.
40
41       -load-ml-object f
42              Load ML object file f.
43
44       -load-ml-source f
45              Load ML file f.
46
47       -l f, -load-vernac-source f
48              Load Coq file f.v (Load f.).
49
50       -lv f, -load-vernac-source-verbose f
51              Load Coq file f.v (Load Verbose f.).
52
53       -load-vernac-object f
54              Load Coq object file f.vo.
55
56       -require f
57              Load Coq object file f.vo and import it (Require f.).
58
59       -compile f
60              Compile Coq file f.v (implies -batch).
61
62       -compile-verbose f
63              Verbosely compile Coq file f.v (implies -batch).
64
65       -opt   Run the native-code version of Coq or Coq_SearchIsos.
66
67       -byte  Run the bytecode version of Coq or Coq_SearchIsos.
68
69       -where Print Coq's standard library location and exit.
70
71       -v     Print Coq version and exit.
72
73       -q     Skip loading of rcfile.
74
75       -init-file f
76              Set the rcfile to f.
77
78       -user u
79              Use the rcfile of user u.
80
81       -batch Batch mode (exits just after arguments parsing).
82
83       -boot  Boot mode (implies -q and -batch).
84
85       -emacs Tells Coq it is executed under Emacs.
86
87       -dump-glob f
88              Dump globalizations in file f (to be used by coqdoc(1)).
89
90       -impredicative-set
91              Set sort Set impredicative.
92
93       -dont-load-proofs
94              Don't load opaque proofs in memory.
95
96       -xml   Export XML files either to the hierarchy rooted in the directory
97              COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).
98
99
100

SEE ALSO

102       coqc(1), coqtop(1), coq-tex(1), coqdep(1).
103       The  Coq  Reference  Manual,  The  Coq  web  site: http://coq.inria.fr,
104       /usr/share/doc/coqide/FAQ.
105
106

AUTHOR

108       This manual page  was  written  by  Samuel  Mimram  <samuel.mimram@ens-
109       lyon.org>, for the Debian project (but may be used by others).
110
111
112
113                                 July 16, 2004                       COQIDE(1)
Impressum