diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-15 13:50:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-15 13:50:24 +0000 |
| commit | 4931e0845f7227e9b4f92ca46f94ac63325ce24f (patch) | |
| tree | d06468be19a82e873edd843d0b2581b583d6f858 /toplevel/usage.ml | |
| parent | 8e83f994d6a4c50857ee25739108eaedc49078da (diff) | |
Ajout nouvelles options
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5208 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6054881f5..d9c3ead2a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -34,6 +34,8 @@ let print_usage_channel co command = -load-ml-source f load ML file f -load-vernac-source f load Coq file f.v (Load f.) -l f (idem) + -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.) + -lv f (idem) -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) @@ -52,7 +54,9 @@ let print_usage_channel co command = -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) - -xml exports XML files either to the hierarchy rooted in + -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) " |