Rechercher une page de manuel
coqide.byte
Langue: en
Version: 251505 (debian - 07/07/09)
Section: 1 (Commandes utilisateur)
NAME
coqide - The Coq Proof Assistant graphical interfaceSYNOPSIS
coqide [ options ]DESCRIPTION
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).
OPTIONS
- -h
- 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.
- -src
- Add source directories in the include path.
- -is f, -inputstate f
- Read state from f.coq.
- -nois
- 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).
- -opt
- Run the native-code version of Coq or Coq_SearchIsos.
- -byte
- Run the bytecode version of Coq or Coq_SearchIsos.
- -where
- Print Coq's standard library location and exit.
- -v
- Print Coq version and exit.
- -q
- Skip loading of rcfile.
- -init-file f
- Set the rcfile to f.
- -user u
- Use the rcfile of user u.
- -batch
- Batch mode (exits just after arguments parsing).
- -boot
- Boot mode (implies -q and -batch).
- -emacs
- Tells Coq it is executed under Emacs.
- -dump-glob f
- Dump globalizations in file f (to be used by coqdoc(1)).
- -impredicative-set
- Set sort Set impredicative.
- -dont-load-proofs
- Don't load opaque proofs in memory.
- -xml
- Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).
SEE ALSO
coqc(1), coqtop(1), coq-tex(1), coqdep(1).
The Coq Reference Manual, The Coq web site: http://coq.inria.fr, /usr/share/doc/coqide/FAQ.
AUTHOR
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, for the Debian project (but may be used by others).Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre