diff options
| author | Vincent Laporte | 2019-05-21 12:39:17 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-21 12:39:17 +0000 |
| commit | 0aa9a5407874332dfa31f1a0f73d2dc91e95fb39 (patch) | |
| tree | 2b1a3cb6418624b9f096479ee58cceb28607f921 /toplevel/usage.ml | |
| parent | 02d6f5660d54fcf4dfc9cff36cbda41dca3f601f (diff) | |
| parent | eed3831a2cc32042fdee95767da00d7e52840371 (diff) | |
Merge PR #10160: Miscellaneous fixes related to the command line
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index da2094653b..29948d50b2 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -42,12 +42,12 @@ let print_usage_common co command = \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ -\n -load-vernac-source f load Coq file f.v (Load f.)\ +\n -load-vernac-source f load Coq file f.v (Load \"f\".)\ \n -l f (idem)\ -\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\ -\n -lv f (idem)\ -\n -load-vernac-object f load Coq object file f.vo\ \n -require path load Coq library path and import it (Require Import path.)\ +\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ +\n -lv f (idem)\ +\n -load-vernac-object path load Coq library path (Require path)\ \n\ \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ @@ -74,9 +74,9 @@ let print_usage_common co command = \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -mangle-names x mangle auto-generated names using prefix x\ -\n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ -\n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ -\n -unset \"Foo Bar\" disable Foo Bar (as Unset Foo Bar. in a file)\ +\n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ +\n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ +\n -unset \"Foo Bar\" disable Foo Bar (as Unset Foo Bar. in a file)\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ @@ -107,7 +107,7 @@ coqtop specific options:\ exit 1 let print_usage_coqc () = - print_usage_common stderr "Usage: coqc <options> <Coq options> file..."; + print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n"; output_string stderr "\n\ coqc specific options:\ \n\ |