diff options
| -rw-r--r-- | toplevel/coqargs.ml | 21 | ||||
| -rw-r--r-- | toplevel/usage.ml | 17 |
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\ |