Rechercher une page de manuel
ssrcoq
Langue: en
Version: 333830 (ubuntu - 24/10/10)
Section: 1 (Commandes utilisateur)
NAME
coqtop - The Coq Proof Assistant toplevel systemSYNOPSIS
coqtop [ options ]DESCRIPTION
coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output.
For batch-oriented use of Coq, see coqc(1).
OPTIONS
- -h, --help
- Help. Will give you the complete list of options accepted by coqtop.
- -I dir, --include dir
- add directory dir in the include path
- -R dir coqdir
- recursively map physical dir to logical coqdir
- -top coqdir
- set the toplevel name to be coqdir instead of Top
- -inputstate filename, -is filename
- read state from file filename.coq
- -nois
- start with an empty intial state
- -outputstatefilename
- write state in file filename.coq
- -load-ml-object filename
- load ML object file filenname
- -load-ml-source filename
- load ML file filename
- -load-vernac-source filename, -l filename
- load Coq file filename.v (Load filename.)
- -load-vernac-source-verbose filename, -lv filename
- load verbosely Coq file filename.v (Load Verbose filename.)
- -load-vernac-object filename
- load Coq object file filename.vo
- -require filename
- load Coq object file filename.vo and import it (Require Import filename.)
- -compile filename
- compile Coq file filename.v (implies -batch )
- -compile-verbose filename
- verbosely compile Coq file filename.v (implies -batch )
- -opt
- run the native-code version of Coq
- -byte
- run the bytecode version of Coq
- -where
- print Coq's standard library location and exit
- -v
- print Coq version and exit
- -q
- skip loading of rcfile
- -init-file filename
- set the rcfile to filename
- -user uid
- use the rcfile of user uid
- -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 filename
- dump globalizations in file f (to be used by coqdoc(1) )
- -with-geoproof (yes|no)
- to (de)activate special functions for Geoproof within Coqide (default is yes )
- -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)
- -quality
- improve the legibility of the proof terms produced by some tactics
SEE ALSO
coqc(1), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr
Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre