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-import 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       -emacs Tells Coq it is executed under Emacs.
69
70       -dump-glob f
71              Dump globalizations in file f (to be used by coqdoc(1)).
72
73       -impredicative-set
74              Set sort Set impredicative.
75
76       -dont-load-proofs
77              Don't load opaque proofs in memory.
78
79

SEE ALSO

81       coqc(1), coqtop(1), coq-tex(1), coqdep(1).
82       The Coq  Reference  Manual,  The  Coq  web  site:  http://coq.inria.fr,
83       /usr/share/doc/coqide/FAQ.
84
85

AUTHOR

87       This  manual  page  was  written  by  Samuel Mimram <samuel.mimram@ens-
88       lyon.org>, for the Debian project (but may be used by others).
89
90
91
92                                                                     COQIDE(1)
Impressum