From 44a5643416fbb0e224cf0031f176bd859ef2faf5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 11 May 2019 22:16:16 +0200 Subject: 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. --- toplevel/usage.ml | 8 ++++---- 1 file 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\ -- cgit v1.2.3