Command line: adding variants for Require, aligning on the vernac syntax.

We deprecate -require (= Require Import) to avoid the confusion with Require.

We propose a regular equivalent to all vernac variants in expanded and
short version:
-require-import, -require-export
-require-import-from, -require-export-from
-ri, -re
-rifrom, -refrom

We also add -rfrom, but wait for the end of deprecation of -require to
replace -load-vernac-object by -require and to introduce a shorthand
-r for the new -require.

2 files changed, 35 insertions, 3 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 4ef31c73b7..9180cae389 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -184,6 +184,10 @@ let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
 
+let warn_deprecated_simple_require =
+  CWarnings.create ~name:"deprecated-boot" ~category:"deprecated"
+         (fun () -> Pp.strbrk "The -require option is deprecated, please use -require-import instead.")
+
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
   { opts with inputstate = Some s }
@@ -416,7 +420,22 @@ let parse_args ~help ~init arglist : t * string list =
       Flags.profile_ltac_cutoff := get_float opt (next ());
       oval
 
-    |"-require" -> add_vo_require oval (next ()) None (Some false)
+    |"-rfrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) None
+
+    |"-require" ->
+      warn_deprecated_simple_require ();
+      add_vo_require oval (next ()) None (Some false)
+
+    |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false)
+
+    |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true)
+
+    |"-require-import-from" | "-rifrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some false)
+
+    |"-require-export-from" | "-refrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some true)
 
     |"-top" ->
       let topname = Libnames.dirpath_of_string (next ()) in
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 29948d50b2..84d3992f5c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -44,10 +44,23 @@ let print_usage_common co command =
 \n  -load-ml-source f      load ML file f\
 \n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
 \n  -l f                   (idem)\
-\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  -load-vernac-object lib, -r lib\
+\n                         load Coq library lib (Require lib)\
+\n  -rfrom root lib        load Coq library lib (From root Require lib.)\
+\n  -require-import lib, -ri lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to Require Import lib.)\
+\n  -require-export lib, -re lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to Require Export lib.)\
+\n  -require-import-from root lib, -rifrom lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to From root Require Import lib.)\
+\n  -require-export-from root lib, -refrom lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to From root Require Export lib.)\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\