diff options
| author | Hugo Herbelin | 2019-05-11 22:16:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:37:50 +0200 |
| commit | 44a5643416fbb0e224cf0031f176bd859ef2faf5 (patch) | |
| tree | b811f4e237eb6c5dc703d088f99947668156ff42 | |
| parent | 00d05ff204108622d1f944d748103a98c0d6d088 (diff) | |
Usage: Fixing wrong description of load_vernac_object and similar.
We also preventively add quoted around Load to suggest that the file
can have "/" in it.
We also fix a too far indentation.
| -rw-r--r-- | toplevel/usage.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 04b23f587f..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\ |