From 4931e0845f7227e9b4f92ca46f94ac63325ce24f Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 15 Jan 2004 13:50:24 +0000 Subject: Ajout nouvelles options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5208 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/usage.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'toplevel/usage.ml') 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) " -- cgit v1.2.3