diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 14:33:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 14:33:35 +0000 |
| commit | 57282991730ee2e864c11868d2498da8aa9eb88b (patch) | |
| tree | 07ff40c95438e43f86970c169f3dfcec6efc6b2b /toplevel/usage.ml | |
| parent | 6d446a63601e5decff645bcf461694218815edfa (diff) | |
MAJ options coqtop et coqc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 9af46b461..4a1f9e4f2 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -23,7 +23,7 @@ let print_usage_channel co command = " -I dir add directory dir in the include path -include dir (idem) -R dir coqdir recursively map physical dir to logical coqdir - -src add source directories in the include path + -top coqdir set the toplevel name to be coqdir instead of Top -inputstate f read state from file f.coq -is f (idem) @@ -35,14 +35,14 @@ let print_usage_channel co command = -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) + -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) -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 + -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 @@ -59,6 +59,9 @@ let print_usage_channel co command = -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 + -h, --help print this list of options " (* print the usage on standard error *) @@ -72,5 +75,6 @@ let print_usage_coqc () = print_usage "Usage: coqc <options> <Coq options> file...\n options are: -verbose compile verbosely + -bindir override the default directory where coqc looks for coqtop -image f specify an alternative executable for Coq -t keep temporary files\n\n" |