Removing -r to prevent the collision with -R.

boot/usage.ml

@@ -40,8 +40,7 @@ let print_usage_common co command =
 \n  -l f                   (idem)\
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
 \n  -lv f	           (idem)\
-\n  -require lib, -r lib\
-\n                         load Coq library lib (Require lib)\
+\n  -require lib           load Coq library lib (Require lib)\
 \n  -require-import lib, -ri lib\
 \n                         load and import Coq library lib\
 \n                         (equivalent to Require Import lib.)\

doc/sphinx/practical-tools/coq-commands.rst

@@ -236,8 +236,10 @@ and ``coqtop``, unless stated otherwise:
 :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the
   Coq script from *file.v*. Write its contents to the standard output as
   it is executed.
-:-r *qualid*, -require *qualid*: Load Coq compiled library :n:`@qualid`.
-  This is equivalent to running :cmd:`Require` :n:`@qualid`.
+:-require *qualid*: Load Coq compiled library :n:`@qualid`.
+  This is equivalent to running :cmd:`Require` :n:`@qualid`
+  (note: the short form `-r *qualid*` is intentionally not provided to
+  prevent the risk of collision with `-R`).
 
   .. _interleave-command-line:
 

man/coqtop.1

@@ -73,7 +73,7 @@ load verbosely Coq file
 (Load Verbose filename.)
 
 .TP
-.BI \-require \ lib, \ \-r \ lib
+.BI \-require \ lib
 load Coq library
 .I lib
 (Require lib.)

sysinit/coqargs.ml

@@ -321,7 +321,7 @@ let parse_args ~usage ~init arglist : t * string list =
       Flags.profile_ltac_cutoff := get_float ~opt (next ());
       oval
 
-    |"-load-vernac-object"|"-require"|"-r" ->
+    |"-load-vernac-object"|"-require" ->
       add_vo_require oval (next ()) None None
 
     |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some Lib.Import)