diff options
| author | Théo Zimmermann | 2020-04-02 15:37:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-02 15:54:11 +0200 |
| commit | 73563c2ff4a4214a3b6aa2333c3f413086500a0e (patch) | |
| tree | e8cee709510faa1d1012d0f3e51aec5613828b91 | |
| parent | 971c8e12078980417c5865948b742dee38bd8593 (diff) | |
Remove deprecated -require option.
This option is confusing because it does Require Import, not Require.
It was deprecated in 8.11. We remove it in 8.12 in order to
reintroduce it in 8.13 as a replacement for -load-vernac-object, which
is the option that does Require without Import as of today.
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 1 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 8 |
2 files changed, 0 insertions, 9 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..85ed0112ae 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -172,7 +172,6 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. -:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only 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) |