diff options
| author | Emilio Jesus Gallego Arias | 2020-04-08 01:48:18 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-08 01:48:18 -0400 |
| commit | b26d1f477990d88e235ffda0f23f494456ce5862 (patch) | |
| tree | 948efae33b55943290a7d6bfe4976eba85caf4c4 /toplevel | |
| parent | 847a42618bc0ff267e5912c6c8f8365f29b158b4 (diff) | |
| parent | 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 (diff) | |
Merge PR #12005: Remove deprecated coqtop options
Ack-by: SkySkimmer
Ack-by: ejgallego
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 4ffbdabf85..1988c7cc42 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -202,10 +202,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 }} @@ -421,10 +417,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) |