Merge PR #12005: Remove deprecated coqtop options

Ack-by: SkySkimmer
Ack-by: ejgallego

6 files changed, 12 insertions, 12 deletions

diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
new file mode 100644
index 0000000000..affb685fcb
--- /dev/null
+++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Confusingly-named and deprecated since 8.11 `-require` option.
+  Use the equivalent `-require-import` instead
+  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
+  by Théo Zimmermann).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index aa4b6edd7d..958d295219 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise:
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
   is equivalent to running :cmd:`Require` :n:`qualid`.
+:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
+  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
@@ -172,7 +174,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/man/coqide.1 b/man/coqide.1
index 62a102af03..c1af046019 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -69,7 +69,7 @@ Load Coq library
 (Require
 .IR path .).
 .TP
-.BI \-require\  path
+.BI \-require-import\  path
 Load Coq library
 .IR path
 and import it (Require Import
diff --git a/man/coqtop.1 b/man/coqtop.1
index 25d0ef7718..e799bc7748 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -79,7 +79,7 @@ load Coq library
 (Require path.)
 
 .TP
-.BI \-require \ path
+.BI \-require-import \ path
 load Coq library
 .I path
 and import it (Require Import path.)
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index c8eb7b08f1..87d844edb3 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -138,7 +138,9 @@ module Make(T : Task) () = struct
           set_slave_opt tl
         (* We need to pass some options with one argument *)
         | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
-          | "-require" | "-w" | "-color" | "-init-file"
+          | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from"
+          | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object"
+          | "-w" | "-color" | "-init-file"
           | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
           | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
           x :: a :: set_slave_opt tl
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)