From 879cacd0a7066a77f10f48f7e7c27e4380f43c9d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 09:38:49 +0200 Subject: Usage: fixing indentation for set/unset options. --- toplevel/usage.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'toplevel/usage.ml') diff --git a/toplevel/usage.ml b/toplevel/usage.ml index da2094653b..3d15cb0274 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -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\ -- cgit v1.2.3 From 00d05ff204108622d1f944d748103a98c0d6d088 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 May 2019 11:20:34 +0200 Subject: Adding missing newline in coqc usage. --- toplevel/usage.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/usage.ml') diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 3d15cb0274..04b23f587f 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -107,7 +107,7 @@ coqtop specific options:\ exit 1 let print_usage_coqc () = - print_usage_common stderr "Usage: coqc file..."; + print_usage_common stderr "Usage: coqc file...\n\n"; output_string stderr "\n\ coqc specific options:\ \n\ -- cgit v1.2.3 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(-) (limited to 'toplevel/usage.ml') 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