diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4963a806f5..d974fc0f7c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -203,10 +203,6 @@ 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 pre = { opts.pre with inputstate = Some s }} @@ -422,10 +418,6 @@ let parse_args ~help ~init arglist : t * string list = |"-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) |