Rechercher une page de manuel

Chercher une autre page de manuel:


Langue: en

Version: 265196 (debian - 07/07/09)

Section: 1 (Commandes utilisateur)


coqide - The Coq Proof Assistant graphical interface


coqide [ options ]


coqtop is a gtk graphical interface for the Coq proof assistant.

For command-line-oriented use of Coq, see coqide(1) ; for batch-oriented use of Coq, see coqc(1).


Show the complete list of options accepted by coqide.
-I dir, -include dir
Add directory dir in the include path.
-R dir coqdir
Recursively map physical dir to logical coqdir.
Add source directories in the include path.
-is f, -inputstate f
Read state from f.coq.
Start with an empty state.
-outputstate f
Write state in file f.coq.
-load-ml-object f
Load ML object file f.
-load-ml-source f
Load ML file f.
-l f, -load-vernac-source f
Load Coq file f.v (Load f.).
-lv f, -load-vernac-source-verbose f
Load Coq file f.v (Load Verbose f.).
-load-vernac-object f
Load Coq object file f.vo.
-require f
Load Coq object file f.vo and import it (Require f.).
-compile f
Compile Coq file f.v (implies -batch).
-compile-verbose f
Verbosely compile Coq file f.v (implies -batch).
Run the native-code version of Coq or Coq_SearchIsos.
Run the bytecode version of Coq or Coq_SearchIsos.
Print Coq's standard library location and exit.
Print Coq version and exit.
Skip loading of rcfile.
-init-file f
Set the rcfile to f.
-user u
Use the rcfile of user u.
Batch mode (exits just after arguments parsing).
Boot mode (implies -q and -batch).
Tells Coq it is executed under Emacs.
-dump-glob f
Dump globalizations in file f (to be used by coqdoc(1)).
Set sort Set impredicative.
Don't load opaque proofs in memory.
Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).


coqc(1), coqtop(1), coq-tex(1), coqdep(1).
The Coq Reference Manual, The Coq web site:, /usr/share/doc/coqide/FAQ.


This manual page was written by Samuel Mimram <>, for the Debian project (but may be used by others).
Comme tu revolutionnes l'informatique pour longtemps, en reduisant a
zero les risques de virus, en reduisant a presque 0 les temps
d'exectution, je pense que la course aux armements qu'es l'evolution des
vitesse d'horloge devient caduque.
-- Jayce - Et oui, je révolutionne le monde du harware aussi. --