diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
| commit | 6497f27021fec4e01f2182014f2bb1989b4707f9 (patch) | |
| tree | 473be7e63895a42966970ab6a70998113bc1bd59 /toplevel/usage.ml | |
| parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) | |
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 9fe8b280..b00cfffc 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml,v 1.15.2.1 2004/07/16 19:31:50 herbelin Exp $ *) +(* $Id: usage.ml,v 1.15.2.2 2004/09/03 14:35:26 herbelin Exp $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" @@ -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" |