diff --git a/dev/ci/user-overlays/21776-ssreflect-prelude.sh b/dev/ci/user-overlays/21776-ssreflect-prelude.sh
new file mode 100644
index 000000000000..4b3a5dc6aba6
--- /dev/null
+++ b/dev/ci/user-overlays/21776-ssreflect-prelude.sh
@@ -0,0 +1,2 @@
+overlay coqutil https://github.com/proux01/coqutil rocq21478 21776
+overlay kami https://github.com/proux01/kami rocq21478 21776
diff --git a/doc/changelog/11-corelib/21776-ssreflect-prelude-Added.rst b/doc/changelog/11-corelib/21776-ssreflect-prelude-Added.rst
new file mode 100644
index 000000000000..fa3fd6c2aa40
--- /dev/null
+++ b/doc/changelog/11-corelib/21776-ssreflect-prelude-Added.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  :ref:`ssreflect <thessreflectprooflanguage>` to the prelude.
+  In extremely rare cases, an extra pair of parentheses may
+  be needed for disambiguation
+  (`#21776 <https://github.com/rocq-prover/rocq/pull/21776>`_,
+  by Pierre Roux).
diff --git a/doc/corelib/hidden-files b/doc/corelib/hidden-files
index 07f50a2f08f7..d6ec45791a05 100644
--- a/doc/corelib/hidden-files
+++ b/doc/corelib/hidden-files
@@ -1,6 +1,6 @@
 theories/Corelib/derive/Derive.v
 theories/Corelib/ssr/ssrsetoid.v
-theories/Corelib/ssr/ssrunder.v
+theories/Corelib/Init/ssrunder.v
 theories/Corelib/extraction/Extraction.v
 theories/Corelib/extraction/ExtrHaskellBasic.v
 theories/Corelib/extraction/ExtrOcamlBasic.v
diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template
index 43b5d3498687..4a2a670217bd 100644
--- a/doc/corelib/index-list.html.template
+++ b/doc/corelib/index-list.html.template
@@ -26,6 +26,9 @@ through the <tt>Require Import</tt> command.</p>
     theories/Corelib/Init/Peano.v
     theories/Corelib/Init/Specif.v
     theories/Corelib/Init/Sumbool.v
+    theories/Corelib/Init/ssrmatching.v
+    theories/Corelib/Init/ssrclasses.v
+    theories/Corelib/Init/ssreflect_rw.v
     theories/Corelib/Init/Tactics.v
     theories/Corelib/Init/Tauto.v
     theories/Corelib/Init/Wf.v
@@ -111,9 +114,6 @@ through the <tt>Require Import</tt> command.</p>
     small scale reflection formalization technique
   </dt>
   <dd>
-    theories/Corelib/ssrmatching/ssrmatching.v
-    theories/Corelib/ssr/ssrclasses.v
-    theories/Corelib/ssr/ssreflect_rw.v
     theories/Corelib/ssr/ssreflect.v
     theories/Corelib/ssr/ssrbool.v
     theories/Corelib/ssr/ssrfun.v
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index f0a5a7666947..bda561615e71 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -212,7 +212,7 @@ Other tokens
   The following character sequences are tokens defined in notations or plugins
   loaded in the :term:`prelude`::
 
-    && ** ++ ... .1 .2 ::= <-> <> >=  /\ \/ || ^ ~
+    && ** ++ ... .1 .2 ::= <-> <> >= /\ \/ || ^ ~ // //= /= =^~
 
   Note that loading additional modules or plugins may expand the set of defined
   tokens.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a94a6d1cdd2d..3ca49c3f10b0 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -85,23 +85,13 @@ Usage
 Getting started
 ~~~~~~~~~~~~~~~
 
-To be available, the tactics presented in this manual need
-``ssreflect_rw.v`` to be loaded.
-
-.. note::
-   One can also load ``ssreflect.v`` to get the deprecated ``rewrite``
-   tactic alias for :tacn:`rw` as well as the ``if <term> is <pattern then _ else _``
-   and ``if <term> isn't <pattern then _ else _`` syntactic sugars for matches
-   and an ``if <term> then _ else _`` syntax specialised to booleans.
-
-Moreover, these tactics come with a methodology
+The tactics presented in this manual come with a methodology
 specific to the authors of |SSR| and which requires a few options
 to be set in a different way than in their default way. All in all,
 this corresponds to working in the following context:
 
 .. rocqtop:: in
 
-   From Corelib Require Import ssreflect_rw.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.
@@ -151,7 +141,6 @@ construct differs from the latter as follows.
 
     .. rocqtop:: reset none
 
-       From Corelib Require Import ssreflect_rw.
        Set Implicit Arguments.
        Unset Strict Implicit.
        Unset Printing Implicit Defensive.
@@ -191,7 +180,7 @@ dependent pattern matching and for aliasing the pattern (see
 Pattern conditional
 ~~~~~~~~~~~~~~~~~~~
 
-When doing ``From Corelib Require Import ssreflect`` (not ``ssreflect_rw``),
+When doing ``From Corelib Require Import ssreflect``,
 the following construct can be used for a refutable pattern matching,
 that is, pattern testing:
 
@@ -314,7 +303,6 @@ expressions such as
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -339,7 +327,6 @@ each point of use; e.g., the above definition can be written:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -451,7 +438,6 @@ For example, the tactic :tacn:`pose (ssreflect)` supports parameters:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -566,7 +552,6 @@ where:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -614,7 +599,6 @@ conditions.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -635,7 +619,6 @@ conditions.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -656,7 +639,6 @@ Moreover:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -676,7 +658,6 @@ Moreover:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -709,7 +690,6 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -731,7 +711,6 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -752,7 +731,6 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -783,7 +761,6 @@ selection.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -800,7 +777,6 @@ only one occurrence of the selected term.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -829,11 +805,7 @@ context of a goal thanks to the ``in`` tactical.
 
   .. example::
 
-     .. rocqtop:: reset none
-
-        From Corelib Require Import ssreflect_rw.
-
-     .. rocqtop:: all
+     .. rocqtop:: reset all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
         set z := 3 in Hx.
@@ -845,11 +817,7 @@ context of a goal thanks to the ``in`` tactical.
 
   .. example::
 
-     .. rocqtop:: reset none
-
-        From Corelib Require Import ssreflect_rw.
-
-     .. rocqtop:: all
+     .. rocqtop:: reset all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
         set z := 3 in Hx * .
@@ -963,7 +931,6 @@ constants to the goal.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1024,7 +991,6 @@ The ``:`` tactical is used to operate on an element in the context.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -1119,7 +1085,6 @@ The move tactic.
 
       .. rocqtop:: reset all
 
-         From Corelib Require Import ssreflect_rw.
          Goal not False.
          move.
 
@@ -1189,7 +1154,6 @@ The elim tactic
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -1229,7 +1193,6 @@ existential metavariables of sort :g:`Prop`.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1409,7 +1372,6 @@ context to interpret wildcards; in particular, it can accommodate the
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1701,7 +1663,6 @@ Clears are deferred until the end of the intro pattern.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1764,7 +1725,6 @@ Block introduction
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -1817,7 +1777,6 @@ deal with the possible parameters of the constants introduced.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1836,7 +1795,6 @@ under fresh |SSR| names.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1903,7 +1861,6 @@ be substituted.
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -2204,7 +2161,6 @@ to the others.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -2323,7 +2279,6 @@ between standard Ltac ``in`` and the |SSR| tactical in.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2398,7 +2353,6 @@ the holes are abstracted in term.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2412,7 +2366,6 @@ the holes are abstracted in term.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2430,7 +2383,6 @@ tactic:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2483,7 +2435,6 @@ the further use of the intermediate step. For instance,
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2511,7 +2462,6 @@ destruction of existential assumptions like in the tactic:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2538,7 +2488,6 @@ term for the intermediate lemma, using tactics of the form:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2567,7 +2516,6 @@ The following example requires the mathcomp and mczify libraries.
 
   .. rocqtop:: all extra-mathcomp extra-mczify
 
-     From Corelib Require Import ssreflect_rw.
      From mathcomp Require Import ssrfun ssrbool ssrnat zify.
 
      Lemma test : True.
@@ -2682,8 +2630,6 @@ typeclass inference.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
-
      Axiom ty : Type.
      Axiom t : ty.
 
@@ -2837,7 +2783,6 @@ The following example requires the mathcomp library.
 
   .. rocqtop:: all extra-mathcomp
 
-     From Corelib Require Import ssreflect_rw.
      From mathcomp Require Import ssrfun ssrbool ssrnat.
 
      Lemma quo_rem_unicity d q1 q2 r1 r2 :
@@ -2861,7 +2806,7 @@ pattern will be used to process its instance.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw ssrfun ssrbool.
+     From Corelib Require Import ssrfun ssrbool.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2911,7 +2856,6 @@ illustrated in the following example.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2930,7 +2874,6 @@ illustrated in the following example.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3063,7 +3006,6 @@ A :token:`r_item` can be one of the following.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -3182,7 +3124,6 @@ proof of basic results on natural numbers arithmetic.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3218,7 +3159,6 @@ side of the equality the user wants to rewrite.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3238,7 +3178,6 @@ the equality.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3261,7 +3200,6 @@ Occurrence switches and redex switches
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3290,7 +3228,6 @@ repetition.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3320,7 +3257,6 @@ rewrite operations prescribed by the rules on the current goal.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3454,7 +3390,6 @@ Anyway this tactic is *not* equivalent to
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3504,7 +3439,6 @@ cases.
 
     .. rocqtop:: reset none
 
-       From Corelib Require Import ssreflect_rw.
        Set Implicit Arguments.
        Unset Strict Implicit.
        Unset Printing Implicit Defensive.
@@ -3620,7 +3554,6 @@ complete terms, as shown by the simple example below.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -3727,8 +3660,7 @@ involves the following steps.
    registered relations (w.r.t. Class ``RewriteRelation``) between a
    term and an evar, e.g., ``m - m = ?F2 m`` in the running example.
    (This support for setoid-like relations is enabled as soon as one does
-   both ``From Corelib Require Import ssreflect_rw.``
-   and ``From Corelib Require Setoid.``)
+   ``From Corelib Require Setoid.``)
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
@@ -3812,7 +3744,6 @@ Notes:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -3944,7 +3875,6 @@ definition.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4057,7 +3987,6 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -4106,7 +4035,6 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -4126,7 +4054,6 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -4305,7 +4232,6 @@ parentheses are required around more complex patterns.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4343,7 +4269,6 @@ Contextual patterns in rewrite
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4582,7 +4507,6 @@ Here is an example of a regular, but nontrivial, eliminator.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4687,7 +4611,6 @@ Here is an example of a truncated eliminator:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4750,7 +4673,6 @@ disjunction.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4771,7 +4693,6 @@ disjunction.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4806,7 +4727,6 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4839,7 +4759,6 @@ relevant for the current goal.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4883,7 +4802,6 @@ assumption to some given arguments.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4911,7 +4829,6 @@ bookkeeping steps.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4969,7 +4886,6 @@ analysis:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4986,7 +4902,6 @@ analysis
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5077,7 +4992,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw ssrbool.
+     From Corelib Require Import ssrbool.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5118,7 +5033,6 @@ The view mechanism is compatible with reflect predicates.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5237,7 +5151,6 @@ but they also allow complex transformation, involving negations.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5271,7 +5184,6 @@ actually uses its propositional interpretation.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5335,7 +5247,6 @@ In this context, the identity view can be used when no view has to be applied:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5352,7 +5263,6 @@ In this context, the identity view can be used when no view has to be applied:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5429,7 +5339,6 @@ pass a given hypothesis to a lemma.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5741,21 +5650,7 @@ Commands
 Compatibility issues
 ~~~~~~~~~~~~~~~~~~~~
 
-Requiring the module `ssreflect_rw` from `Corelib`
-creates an environment that is mostly
-compatible with the rest of Rocq, up to a few discrepancies.
-
-+ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`,
-  :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`)
-  might clash with user tactic names.
-+ New symbols (``//``, ``/=``, ``//=``) might clash with adjacent
-  existing symbols.
-  This can be avoided by inserting white spaces.
-+ Some user notations (in particular, defining an infix ``;``) might
-  interfere with the "open term", parenthesis-free syntax of tactics
-  such as :tacn:`have`, :tacn:`set (ssreflect)` and :tacn:`pose (ssreflect)`.
-
-In addition, requiring the backward compatibility module `ssreflect` from `Corelib`
+Requiring the backward compatibility module `ssreflect` from `Corelib`
 creates an environment that is mostly
 compatible with the rest of Rocq, up to a few discrepancies.
 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 08118e3f1874..e4e6063be2ad 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -500,7 +500,7 @@ $(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISI
 	  output=$*.out.real; \
 	  export LC_CTYPE=C; \
 	  export LANG=C; \
-	  $(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" -norec $(shell basename $< .v) > $$output 2>&1) ; \
+	  $(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" $(shell basename $< .v) > $$output 2>&1) ; \
 	  diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
diff --git a/test-suite/output-coqtop/LevelTolerance.out b/test-suite/output-coqtop/LevelTolerance.out
index 1518a522a9a1..97e0afb31169 100644
--- a/test-suite/output-coqtop/LevelTolerance.out
+++ b/test-suite/output-coqtop/LevelTolerance.out
@@ -567,6 +567,9 @@ Rocq < Rocq < Entry ltac_expr is
   [ IDENT "atom5" ]
 | "4" LEFTA
   [ SELF; IDENT "post44"
+  | SELF; ";"; IDENT "first"; ssr_first_else
+  | SELF; ";"; IDENT "first"; ssrseqarg
+  | SELF; ";"; IDENT "last"; ssrseqarg
   | SELF; ";"; SELF
   | SELF; ";"; tactic_then_locality; for_each_goal; "]"
   | IDENT "pre43"; NEXT
@@ -575,6 +578,9 @@ Rocq < Rocq < Entry ltac_expr is
 | "3" RIGHTA
   [ "atom3"
   | IDENT "try"; SELF
+  | IDENT "do"; ssrmmod; ssrdotac; ssrclauses; LIST0 ssrintros_ne
+  | IDENT "do"; ssrortacarg; ssrclauses; LIST0 ssrintros_ne
+  | IDENT "do"; nat_or_var; ssrmmod; ssrdotac; ssrclauses; LIST0 ssrintros_ne
   | IDENT "do"; nat_or_var; SELF
   | IDENT "timeout"; nat_or_var; SELF
   | IDENT "time"; OPT string; SELF
@@ -582,6 +588,7 @@ Rocq < Rocq < Entry ltac_expr is
   | IDENT "progress"; SELF
   | IDENT "once"; SELF
   | IDENT "exactly_once"; SELF
+  | IDENT "abstract"; ssrdgens
   | IDENT "abstract"; NEXT; "using"; ident
   | IDENT "abstract"; NEXT
   | IDENT "only"; goal_selector; ":"; SELF ]
@@ -594,7 +601,7 @@ Rocq < Rocq < Entry ltac_expr is
   | "atom2"
   | IDENT "tryif"; SELF; "then"; SELF; "else"; SELF ]
 | "1l" LEFTA
-  [  ]
+  [ SELF; ssrintros_ne ]
 | "1" RIGHTA
   [ "atom1"
   | "fun"; LIST1 input_fun; "=>"; ltac_expr LEVEL "5"
@@ -614,6 +621,7 @@ Rocq < Rocq < Entry ltac_expr is
 | "0" LEFTA
   [ "("; SELF; ")"
   | "["; ">"; for_each_goal; "]"
+  | ssrparentacarg
   | tactic_atom ] ]
 
 Entry simple_tactic is
@@ -623,6 +631,35 @@ Entry simple_tactic is
   | IDENT "firstorder"; OPT tactic; firstorder_using
   | IDENT "congruence"; OPT natural; "with"; LIST1 constr
   | IDENT "congruence"; OPT natural
+  | IDENT "under"; ssrrwarg; IDENT "do"; ssrhint3arg
+  | IDENT "under"; ssrrwarg; ssrintros_ne; IDENT "do"; ssrhint3arg
+  | IDENT "under"; ssrrwarg; ssrintros_ne
+  | IDENT "under"; ssrrwarg
+  | IDENT "generally"; IDENT "have"; ssrclear; ssr_idcomma; ssrhpats_nobs;
+    ssrwlogfwd; ssrhint
+  | IDENT "gen"; IDENT "have"; ssrclear; ssr_idcomma; ssrhpats_nobs;
+    ssrwlogfwd; ssrhint
+  | IDENT "without"; IDENT "loss"; IDENT "suffices"; ssrhpats_nobs;
+    ssrwlogfwd; ssrhint
+  | IDENT "without"; IDENT "loss"; IDENT "suff"; ssrhpats_nobs; ssrwlogfwd;
+    ssrhint
+  | IDENT "without"; IDENT "loss"; ssrhpats_nobs; ssrwlogfwd; ssrhint
+  | IDENT "wlog"; IDENT "suffices"; ssrhpats_nobs; ssrwlogfwd; ssrhint
+  | IDENT "wlog"; IDENT "suff"; ssrhpats_nobs; ssrwlogfwd; ssrhint
+  | IDENT "wlog"; ssrhpats_nobs; ssrwlogfwd; ssrhint
+  | IDENT "suffices"; IDENT "have"; ssrhpats_nobs; ssrhavefwd
+  | IDENT "suffices"; ssrsufffwd
+  | IDENT "suff"; IDENT "have"; ssrhpats_nobs; ssrhavefwd
+  | IDENT "suff"; ssrsufffwd
+  | IDENT "have"; IDENT "suffices"; ssrhpats_nobs; ssrhavefwd
+  | IDENT "have"; IDENT "suff"; ssrhpats_nobs; ssrhavefwd
+  | IDENT "have"; ssrhavefwdwbinders
+  | IDENT "unlock"; ssrunlockargs; ssrclauses
+  | IDENT "rw"; ssrrwargs; ssrclauses
+  | IDENT "ssrinstancesofruleR2L"; ssrterm
+  | IDENT "ssrinstancesofruleL2R"; ssrterm
+  | IDENT "congr"; ssrcongrarg
+  | "by"; ssrhintarg
   | IDENT "dintuition"; tactic
   | IDENT "dintuition"
   | IDENT "intuition"; tactic
@@ -641,14 +678,19 @@ Entry simple_tactic is
   | IDENT "clearbody"; LIST1 hyp
   | IDENT "clear"; IDENT "dependent"; hyp
   | IDENT "clear"; "-"; LIST1 hyp
+  | IDENT "clear"; natural
   | IDENT "clear"; LIST0 hyp
   | IDENT "revert"; IDENT "dependent"; hyp
   | IDENT "revert"; LIST1 hyp
   | IDENT "rename"; LIST1 rename SEP ","
+  | IDENT "move"; ssrmovearg; ssrrpat
+  | IDENT "move"; ssrmovearg; ssrclauses
+  | IDENT "move"; ssrrpat
   | IDENT "move"; hyp; "at"; IDENT "top"
   | IDENT "move"; hyp; "at"; IDENT "bottom"
   | IDENT "move"; hyp; IDENT "after"; hyp
   | IDENT "move"; hyp; IDENT "before"; hyp
+  | IDENT "move"
   | IDENT "intro"; "at"; IDENT "top"
   | IDENT "intro"; "at"; IDENT "bottom"
   | IDENT "intro"; IDENT "after"; hyp
@@ -678,7 +720,10 @@ Entry simple_tactic is
   | IDENT "right"; "with"; bindings
   | IDENT "eleft"; "with"; bindings
   | IDENT "left"; "with"; bindings
+  | IDENT "exact"; "<:"; lconstr
+  | IDENT "exact"; ssrexactarg
   | IDENT "exact"; uconstr
+  | IDENT "exact"
   | IDENT "with_strategy"; strategy_level_or_var; "["; LIST1 smart_global;
     "]"; ltac_expr LEVEL "3"
   | IDENT "guard"; test
@@ -796,16 +841,23 @@ Entry simple_tactic is
   | IDENT "apply"; "<-"; constr
   | IDENT "apply"; "->"; constr; "in"; hyp
   | IDENT "apply"; "->"; constr
+  | IDENT "apply"; ssrapplyarg
   | IDENT "apply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
+  | IDENT "apply"
   | IDENT "eapply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
+  | IDENT "elim"; ssrarg; ssrclauses
   | IDENT "elim"; constr_with_bindings_arg; OPT eliminator
+  | IDENT "elim"
   | IDENT "eelim"; constr_with_bindings_arg; OPT eliminator
+  | IDENT "case"; ssrcasearg; ssrclauses
   | IDENT "case"; induction_clause_list
+  | IDENT "case"
   | IDENT "ecase"; induction_clause_list
   | "fix"; ident; natural; "with"; LIST1 fixdecl
   | "fix"; ident; natural
   | "cofix"; ident; "with"; LIST1 cofixdecl
   | "cofix"; ident
+  | IDENT "set"; ssrfwdid; ssrsetfwd; ssrclauses
   | IDENT "set"; bindings_with_parameters; clause
   | IDENT "set"; constr; as_name; clause
   | IDENT "eset"; bindings_with_parameters; clause
@@ -823,6 +875,9 @@ Entry simple_tactic is
   | IDENT "pose"; IDENT "proof"; lpar_id_coloneq; "("; identref; ":=";
     lconstr; ")"
   | IDENT "pose"; IDENT "proof"; lconstr; as_ipat
+  | IDENT "pose"; ssrfixfwd
+  | IDENT "pose"; ssrcofixfwd
+  | IDENT "pose"; ssrfwdid; ssrposefwd
   | IDENT "pose"; bindings_with_parameters
   | IDENT "pose"; constr; as_name
   | IDENT "epose"; IDENT "proof"; lpar_id_coloneq; "("; identref; ":=";
@@ -902,6 +957,91 @@ Entry simple_tactic is
 Entry tactic_value is
 [ LEFTA
   [ IDENT "firstorder_using"; ":"; "("; firstorder_using; ")"
+  | IDENT "ssr_idcomma"; ":"; "("; ssr_idcomma; ")"
+  | IDENT "ssrwlogfwd"; ":"; "("; ssrwlogfwd; ")"
+  | IDENT "ssrsufffwd"; ":"; "("; ssrsufffwd; ")"
+  | IDENT "ssrunlockargs"; ":"; "("; ssrunlockargs; ")"
+  | IDENT "ssrunlockarg"; ":"; "("; ssrunlockarg; ")"
+  | IDENT "ssrrwargs"; ":"; "("; ssrrwargs; ")"
+  | IDENT "ssrrwarg"; ":"; "("; ssrrwarg; ")"
+  | IDENT "ssrpattern_ne_squarep"; ":"; "("; ssrpattern_ne_squarep; ")"
+  | IDENT "ssrpattern_squarep"; ":"; "("; ssrpattern_squarep; ")"
+  | IDENT "ssrrule"; ":"; "("; ssrrule; ")"
+  | IDENT "ssrrule_ne"; ":"; "("; ssrrule_ne; ")"
+  | IDENT "ssrrwocc"; ":"; "("; ssrrwocc; ")"
+  | IDENT "ssrcongrarg"; ":"; "("; ssrcongrarg; ")"
+  | IDENT "ssrexactarg"; ":"; "("; ssrexactarg; ")"
+  | IDENT "ssrapplyarg"; ":"; "("; ssrapplyarg; ")"
+  | IDENT "ssragens"; ":"; "("; ssragens; ")"
+  | IDENT "ssragen"; ":"; "("; ssragen; ")"
+  | IDENT "ssrcasearg"; ":"; "("; ssrcasearg; ")"
+  | IDENT "ssrmovearg"; ":"; "("; ssrmovearg; ")"
+  | IDENT "ssrarg"; ":"; "("; ssrarg; ")"
+  | IDENT "ssreqid"; ":"; "("; ssreqid; ")"
+  | IDENT "ssrdgens"; ":"; "("; ssrdgens; ")"
+  | IDENT "ssrdgens_tl"; ":"; "("; ssrdgens_tl; ")"
+  | IDENT "ssrgen"; ":"; "("; ssrgen; ")"
+  | IDENT "ssrseqdir"; ":"; "("; ssrseqdir; ")"
+  | IDENT "ssrseqarg"; ":"; "("; ssrseqarg; ")"
+  | IDENT "ssrdoarg"; ":"; "("; ssrdoarg; ")"
+  | IDENT "ssrhavefwdwbinders"; ":"; "("; ssrhavefwdwbinders; ")"
+  | IDENT "ssrhavefwd"; ":"; "("; ssrhavefwd; ")"
+  | IDENT "ssrsetfwd"; ":"; "("; ssrsetfwd; ")"
+  | IDENT "ssrcofixfwd"; ":"; "("; ssrcofixfwd; ")"
+  | IDENT "ssrfixfwd"; ":"; "("; ssrfixfwd; ")"
+  | IDENT "ssrposefwd"; ":"; "("; ssrposefwd; ")"
+  | IDENT "ssrstruct"; ":"; "("; ssrstruct; ")"
+  | IDENT "ssrbinder"; ":"; "("; ssrbinder; ")"
+  | IDENT "ssrbvar"; ":"; "("; ssrbvar; ")"
+  | IDENT "ssrfwd"; ":"; "("; ssrfwd; ")"
+  | IDENT "ssrclauses"; ":"; "("; ssrclauses; ")"
+  | IDENT "ssrclausehyps"; ":"; "("; ssrclausehyps; ")"
+  | IDENT "ssrwgen"; ":"; "("; ssrwgen; ")"
+  | IDENT "ssrhint"; ":"; "("; ssrhint; ")"
+  | IDENT "ssrortacarg"; ":"; "("; ssrortacarg; ")"
+  | IDENT "ssrhint3arg"; ":"; "("; ssrhint3arg; ")"
+  | IDENT "ssrhintarg"; ":"; "("; ssrhintarg; ")"
+  | IDENT "ssrortacs"; ":"; "("; ssrortacs; ")"
+  | IDENT "ssrfwdid"; ":"; "("; ssrfwdid; ")"
+  | IDENT "ssrintrosarg"; ":"; "("; ssrintrosarg; ")"
+  | IDENT "ssrintros"; ":"; "("; ssrintros; ")"
+  | IDENT "ssrintros_ne"; ":"; "("; ssrintros_ne; ")"
+  | IDENT "ssrrpat"; ":"; "("; ssrrpat; ")"
+  | IDENT "ssrhpats_nobs"; ":"; "("; ssrhpats_nobs; ")"
+  | IDENT "ssrhpats_wtransp"; ":"; "("; ssrhpats_wtransp; ")"
+  | IDENT "ssrhpats"; ":"; "("; ssrhpats; ")"
+  | IDENT "ssripats_ne"; ":"; "("; ssripats_ne; ")"
+  | IDENT "ssrcpat"; ":"; "("; ssrcpat; ")"
+  | IDENT "ssriorpat"; ":"; "("; ssriorpat; ")"
+  | IDENT "ssripats"; ":"; "("; ssripats; ")"
+  | IDENT "ssripat"; ":"; "("; ssripat; ")"
+  | IDENT "ident_no_do"; ":"; "("; ident_no_do; ")"
+  | IDENT "ssrfwdview"; ":"; "("; ssrfwdview; ")"
+  | IDENT "ssrbwdview"; ":"; "("; ssrbwdview; ")"
+  | IDENT "ast_closure_lterm"; ":"; "("; ast_closure_lterm; ")"
+  | IDENT "ast_closure_term"; ":"; "("; ast_closure_term; ")"
+  | IDENT "ssrterm"; ":"; "("; ssrterm; ")"
+  | IDENT "ssrdocc"; ":"; "("; ssrdocc; ")"
+  | IDENT "ssrmult"; ":"; "("; ssrmult; ")"
+  | IDENT "ssrmult_ne"; ":"; "("; ssrmult_ne; ")"
+  | IDENT "ssrocc"; ":"; "("; ssrocc; ")"
+  | IDENT "ssrindex"; ":"; "("; ssrindex; ")"
+  | IDENT "ssrclear"; ":"; "("; ssrclear; ")"
+  | IDENT "ssrclear_ne"; ":"; "("; ssrclear_ne; ")"
+  | IDENT "ssrsimpl_ne"; ":"; "("; ssrsimpl_ne; ")"
+  | IDENT "ssrhoi_id"; ":"; "("; ssrhoi_id; ")"
+  | IDENT "ssrhoi_hyp"; ":"; "("; ssrhoi_hyp; ")"
+  | IDENT "ssrhyp"; ":"; "("; ssrhyp; ")"
+  | IDENT "ssrtclarg"; ":"; "("; ssrtacarg; ")"
+  | IDENT "ssrtac3arg"; ":"; "("; ssrtac3arg; ")"
+  | IDENT "ssrtacarg"; ":"; "("; ssrtacarg; ")"
+  | IDENT "ssrviewposspc"; ":"; "("; ssrviewpos; ")"
+  | IDENT "ssrviewpos"; ":"; "("; ssrviewpos; ")"
+  | IDENT "ssrhintref"; ":"; "("; ssrhintref; ")"
+  | IDENT "ssrpatternarg"; ":"; "("; rpattern; ")"
+  | IDENT "lcpattern"; ":"; "("; lcpattern; ")"
+  | IDENT "cpattern"; ":"; "("; cpattern; ")"
+  | IDENT "rpattern"; ":"; "("; rpattern; ")"
   | IDENT "test"; ":"; "("; test; ")"
   | IDENT "comparison"; ":"; "("; comparison; ")"
   | IDENT "opthints"; ":"; "("; opthints; ")"
diff --git a/test-suite/output/PrintGrammar.out b/test-suite/output/PrintGrammar.out
index 1724e7df811f..4c77130199ae 100644
--- a/test-suite/output/PrintGrammar.out
+++ b/test-suite/output/PrintGrammar.out
@@ -14,7 +14,8 @@ Entry term is
   [ SELF; "<:"; term LEVEL "200"
   | SELF; "<<:"; term LEVEL "200"
   | SELF; ":>"; term LEVEL "200"
-  | SELF; ":"; term LEVEL "200" ]
+  | SELF; ":"; term LEVEL "200"
+  | "=^~"; NEXT ]
 | "99" RIGHTA
   [ SELF; "->"; term LEVEL "200" ]
 | "95" RIGHTA
@@ -72,6 +73,10 @@ Entry term is
   | "@"; pattern_ident; LIST1 identref
   | "forall"; open_binders; ","; term LEVEL "200"
   | "fun"; open_binders; "=>"; term LEVEL "200"
+  | "let"; ":"; ssr_mpat; ":="; lconstr; "in"; lconstr
+  | "let"; ":"; ssr_mpat; ":="; lconstr; ssr_rtype; "in"; lconstr
+  | "let"; ":"; ssr_mpat; "in"; pattern; ":="; lconstr; ssr_rtype; "in";
+    lconstr
   | "let"; "fix"; fix_decl; "in"; term LEVEL "200"
   | "let"; "cofix"; cofix_body; "in"; term LEVEL "200"
   | "let"; "'"; pattern LEVEL "200"; OPT [ "in"; pattern LEVEL "200" ]; ":=";
@@ -96,7 +101,20 @@ Entry term is
   | SELF; "%"; IDENT
   | SELF; "%_"; IDENT ]
 | "0" LEFTA
-  [ "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "&"; term LEVEL
+  [ "["; "!"; term LEVEL "200"; "]"
+  | "["; NUMBER "1"; "!"; term LEVEL "200"; "]"
+  | "["; IDENT "dup"; "]"
+  | "["; IDENT "swap"; "]"
+  | "["; IDENT "apply"; "]"
+  | "["; IDENT "elaborate"; term LEVEL "200"; "]"
+  | "["; IDENT "unlockable"; "fun"; term LEVEL "200"; "]"
+  | "["; IDENT "unlockable"; "of"; term LEVEL "200"; "]"
+  | "["; IDENT "the"; term LEVEL "200"; "of"; term LEVEL "200"; "]"
+  | "["; IDENT "the"; term LEVEL "200"; "of"; term LEVEL "200"; "by"; term
+    LEVEL "200"; "]"
+  | "(*******"; "//"; "/="; "//="; "*******)"
+  | "{"; IDENT "type"; "of"; term LEVEL "200"; "for"; term LEVEL "200"; "}"
+  | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "&"; term LEVEL
     "200"; "}"
   | "{"; "'"; pattern LEVEL "0"; "&"; term LEVEL "200"; "}"
   | "{"; "'"; pattern LEVEL "0"; ":"; term LEVEL "200"; "&"; term LEVEL
@@ -122,6 +140,12 @@ Entry term is
   | "{"; term LEVEL "99"; "|"; term LEVEL "200"; "}"
   | "{"; term LEVEL "99"; "}"
   | IDENT "ltac"; ":"; "("; ltac_expr; ")"
+  | "("; term LEVEL "200"; "as"; term LEVEL "200"; "in"; term LEVEL "200";
+    ")"
+  | "("; term LEVEL "200"; "as"; term LEVEL "200"; ")"
+  | "("; term LEVEL "200"; "in"; term LEVEL "200"; "in"; term LEVEL "200";
+    ")"
+  | "("; term LEVEL "200"; "in"; term LEVEL "200"; ")"
   | "("; term LEVEL "200"; ","; term LEVEL "200"; ","; LIST1 (term LEVEL
     "200") SEP ","; ")"
   | "("; term LEVEL "200"; ","; term LEVEL "200"; ")"
diff --git a/test-suite/output/PrintKeywords.out b/test-suite/output/PrintKeywords.out
index 7dc6175218a7..f5cbacfc5039 100644
--- a/test-suite/output/PrintKeywords.out
+++ b/test-suite/output/PrintKeywords.out
@@ -8,9 +8,11 @@
 '
 (
 ()
+(*******
 )
 *
 **
+*******)
 +
 ++
 ,
@@ -23,6 +25,9 @@
 .1
 .2
 /
+//
+//=
+/=
 /\
 :
 ::
@@ -41,6 +46,7 @@
 <>
 =
 =>
+=^~
 >
 >->
 >=
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 1e5d2617bee9..2ead3a98dd3d 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -20,6 +20,7 @@ le_sind:
   forall n0 : nat, n <= n0 -> P n0
 false: bool
 true: bool
+NonPropType.test_of: bool -> Set
 is_true: bool -> Prop
 eq_true: bool -> Prop
 negb: bool -> bool
@@ -29,88 +30,105 @@ reflect: Prop -> bool -> Set
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
 Nat.even: nat -> bool
+NonPropType.result: nonPropType -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
+Number.uint_beq: Number.uint -> Number.uint -> bool
+Nat.eqb: nat -> nat -> bool
+Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 Nat.leb: nat -> nat -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
-Number.uint_beq: Number.uint -> Number.uint -> bool
+NonPropType.call_of: unit -> bool -> Type
 Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
 Decimal.signed_int_beq: Decimal.signed_int -> Decimal.signed_int -> bool
-Nat.eqb: nat -> nat -> bool
-Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Nat.ltb: nat -> nat -> bool
-Number.number_beq: Number.number -> Number.number -> bool
+Nat.testbit: nat -> nat -> bool
 Hexadecimal.signed_int_beq:
   Hexadecimal.signed_int -> Hexadecimal.signed_int -> bool
+Number.number_beq: Number.number -> Number.number -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
-Nat.testbit: nat -> nat -> bool
+NonPropType.Test: forall result : bool, unit -> NonPropType.test_of result
+NonPropType.condition:
+  forall [result : bool], NonPropType.test_of result -> unit
+NonPropType.callee:
+  forall [condition : unit] [result : bool],
+  NonPropType.call_of condition result -> Type
+NonPropType.Call:
+  forall (condition : unit) (result : bool),
+  Type -> NonPropType.call_of condition result
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-eq_true_rew_r:
-  forall [b : bool] (P : bool -> Type), P b -> eq_true b -> P true
-eq_true_rew:
-  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
-bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-eq_true_rec_r:
-  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall [b : bool], eq_true b -> P b
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
-eq_true_rect_r:
-  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
-eq_true_rec:
-  forall P : bool -> Set, P true -> forall [b : bool], eq_true b -> P b
 eq_true_ind_r:
   forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall [b : bool], eq_true b -> P b
+eq_true_rew:
+  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
 eq_true_sind:
   forall P : bool -> SProp, P true -> forall [b : bool], eq_true b -> P b
 bool_sind:
   forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
+eq_true_rew_r:
+  forall [b : bool] (P : bool -> Type), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
+eq_true_rec:
+  forall P : bool -> Set, P true -> forall [b : bool], eq_true b -> P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 bool_of_sumbool:
   forall [A B : Prop], {A} + {B} -> {b : bool | if b then A else B}
 sumbool_of_bool: forall b : bool, {b = true} + {b = false}
+NonPropType.check:
+  forall [result : bool] [test : NonPropType.test_of result],
+  NonPropType.call_of (NonPropType.condition test) result -> nonPropType
+NonPropType.Check:
+  forall [result : bool] [test : NonPropType.test_of result],
+  NonPropType.call_of (NonPropType.condition test) result -> nonPropType
 Decimal.internal_signed_int_dec_lb:
   forall x y : Decimal.signed_int, x = y -> Decimal.signed_int_beq x y = true
-Number.internal_signed_int_dec_lb1:
-  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
-Number.internal_signed_int_dec_bl1:
-  forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
 Decimal.internal_signed_int_dec_bl:
   forall x y : Decimal.signed_int, Decimal.signed_int_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
-Hexadecimal.internal_signed_int_dec_lb0:
-  forall x y : Hexadecimal.signed_int,
-  x = y -> Hexadecimal.signed_int_beq x y = true
-Number.internal_number_dec_lb:
-  forall x y : Number.number, x = y -> Number.number_beq x y = true
-Hexadecimal.internal_signed_int_dec_bl0:
-  forall x y : Hexadecimal.signed_int,
-  Hexadecimal.signed_int_beq x y = true -> x = y
-Number.internal_uint_dec_lb1:
-  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
-Number.internal_uint_dec_bl1:
-  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
 Decimal.internal_decimal_dec_bl:
   forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Number.internal_signed_int_dec_lb1:
+  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
+Number.internal_signed_int_dec_bl1:
+  forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
 Number.internal_number_dec_bl:
   forall x y : Number.number, Number.number_beq x y = true -> x = y
-Byte.of_bits:
-  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
-  Byte.byte
 Byte.to_bits:
   Byte.byte ->
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
+Hexadecimal.internal_signed_int_dec_bl0:
+  forall x y : Hexadecimal.signed_int,
+  Hexadecimal.signed_int_beq x y = true -> x = y
 Decimal.internal_decimal_dec_lb:
   forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
-Hexadecimal.internal_hexadecimal_dec_bl:
-  forall x y : Hexadecimal.hexadecimal,
-  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Hexadecimal.internal_signed_int_dec_lb0:
+  forall x y : Hexadecimal.signed_int,
+  x = y -> Hexadecimal.signed_int_beq x y = true
+Number.internal_number_dec_lb:
+  forall x y : Number.number, x = y -> Number.number_beq x y = true
+Byte.of_bits:
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
+  Byte.byte
 eq_true_rew_fwd_dep:
   forall [b : bool] (H : eq_true b)
     (P : forall b0 : bool, eq_true b0 -> Type),
@@ -118,14 +136,6 @@ eq_true_rew_fwd_dep:
 eq_true_rew_dep:
   forall P : forall b : bool, eq_true b -> Type,
   P true is_eq_true -> forall [b : bool] (e : eq_true b), P b e
-Decimal.internal_uint_dec_bl:
-  forall x : Decimal.uint,
-  (fun x0 : Decimal.uint =>
-   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
-Decimal.internal_uint_dec_lb:
-  forall x : Decimal.uint,
-  (fun x0 : Decimal.uint =>
-   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
 Hexadecimal.internal_uint_dec_lb0:
   forall x : Hexadecimal.uint,
   (fun x0 : Hexadecimal.uint =>
@@ -134,9 +144,17 @@ Hexadecimal.internal_uint_dec_bl0:
   forall x : Hexadecimal.uint,
   (fun x0 : Hexadecimal.uint =>
    forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_eq_rec:
   forall (b : bool) (P : bool -> Set),
   (b = true -> P true) -> (b = false -> P false) -> P b
@@ -151,23 +169,23 @@ BoolSpec_ind:
   forall [P Q : Prop] (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall [b : bool], BoolSpec P Q b -> P0 b
-reflect_ind:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Prop),
+reflect_rect:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Type),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_sind:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> SProp),
+reflect_rec:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_rect:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Type),
+reflect_sind:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> SProp),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_rec:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
+reflect_ind:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Prop),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 4a06c5c6eb78..6be7c0a22b02 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,19 +1,20 @@
 false: bool
 true: bool
 negb: bool -> bool
-xorb: bool -> bool -> bool
 andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+xorb: bool -> bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+NonPropType.result: nonPropType -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 Number.uint_beq: Number.uint -> Number.uint -> bool
 Nat.testbit: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
 Number.number_beq: Number.number -> Number.number -> bool
 Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
 Hexadecimal.signed_int_beq:
@@ -95,9 +96,18 @@ iff_refl: forall A : Prop, A <-> A
 le_n: forall n : nat, n <= n
 eq_refl: forall {A : Type} {x : A}, x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
+ssrclasses.reflexivity:
+  forall {A : Type} {R : A -> A -> Prop},
+  ssrclasses.Reflexive R -> forall x : A, R x x
 refl:
   forall {eq : forall A : Type@{β0 ; _}, A -> A -> Type@{β1 ; _}},
   Has_refl eq -> forall (A : Type@{β0 ; _}) (x : A), eq A x x
+over_rel_done:
+  forall (A : Type) (eqA : A -> A -> Prop),
+  ssrclasses.Reflexive eqA -> forall x : A, Over_rel A eqA x x
+under_rel_done:
+  forall (A : Type) (eqA : A -> A -> Prop),
+  ssrclasses.Reflexive eqA -> forall x : A, 'Under[ x ]
 (use "About" for full details on the implicit arguments of eq_refl)
 conj: forall [A B : Prop], A -> B -> A /\ B
 pair: forall {A B : Type}, A -> B -> A * B
diff --git a/test-suite/output/Search_headconcl.out b/test-suite/output/Search_headconcl.out
index b6b2f536b0fa..0aee6494ecc9 100644
--- a/test-suite/output/Search_headconcl.out
+++ b/test-suite/output/Search_headconcl.out
@@ -7,19 +7,20 @@ le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
 true: bool
 negb: bool -> bool
-xorb: bool -> bool -> bool
 andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+xorb: bool -> bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+NonPropType.result: nonPropType -> bool
 Nat.odd: nat -> bool
 Nat.even: nat -> bool
 Number.uint_beq: Number.uint -> Number.uint -> bool
 Nat.testbit: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
 Number.number_beq: Number.number -> Number.number -> bool
 Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
 Hexadecimal.signed_int_beq:
diff --git a/test-suite/output/bug_16224.out b/test-suite/output/bug_16224.out
index eb93946c7d42..03374683ecaa 100644
--- a/test-suite/output/bug_16224.out
+++ b/test-suite/output/bug_16224.out
@@ -2,6 +2,9 @@
 [cic] : Cic >-> A (reversible)
 [rc] : Rc >-> A (reversible)
 [ric] : Ric >-> A (reversible)
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 ric : Ric -> A
 cic : Cic -> A
 ri : Ri -> A
diff --git a/test-suite/output/ltac2_printabout.out b/test-suite/output/ltac2_printabout.out
index be81b069173f..f6ce99416860 100644
--- a/test-suite/output/ltac2_printabout.out
+++ b/test-suite/output/ltac2_printabout.out
@@ -3,6 +3,8 @@ snd : 'b * 'a -> 'a
 type : constr -> constr
 Ltac2 type : constr -> constr
       type := @external "rocq-runtime.plugins.ltac2" "constr_type"
+Inductive Corelib.Init.ssreflect_rw.NonPropType.type
+  (shorter name to refer to it in current context is NonPropType.type)
 Ltac2 ltac2_printabout.type
 Ltac2 type : constr -> constr
 None : 'a option
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index 906a6a6ffc99..4ccad52f9c52 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -19,6 +19,9 @@ New coercion path [h1; f3] : B >-> C' is ambiguous with existing
 [h2] : B' >-> C'
 [f3] : C >-> C'
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 File "./output/relaxed_ambiguous_paths.v", line 33, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
@@ -30,6 +33,9 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [bc; cd] : B >-> D
 [cd] : C >-> D
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 File "./output/relaxed_ambiguous_paths.v", line 50, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
@@ -44,12 +50,18 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
 [ba] : B >-> A
 [bc] : B >-> C
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_A] : D >-> A
 [D_B] : D >-> B
 [D_C] : D >-> C
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 [A'_A] : A' >-> A
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [B_A'; A'_A] : B >-> A
@@ -60,6 +72,9 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 File "./output/relaxed_ambiguous_paths.v", line 147, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
@@ -74,6 +89,9 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
+[NonPropType.callee] : NonPropType.call_of >-> Sortclass
+[NonPropType.frame; NonPropType.callee] : NonPropType.type >-> Sortclass
+[NonPropType.frame] : NonPropType.type >-> NonPropType.call_of
 File "./output/relaxed_ambiguous_paths.v", line 156, characters 0-47:
 Warning:
 New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
diff --git a/theories/Corelib/Init/Prelude.v b/theories/Corelib/Init/Prelude.v
index f7041e993b61..f467d7326acf 100644
--- a/theories/Corelib/Init/Prelude.v
+++ b/theories/Corelib/Init/Prelude.v
@@ -24,6 +24,7 @@ Require Export Corelib.Init.Ltac.
 Require Export Corelib.Init.Tactics.
 Require Export Corelib.Init.Tauto.
 Require Export Corelib.Init.Sumbool.
+Require Export ssreflect_rw.
 (* Some initially available plugins. See also:
    - ltac_plugin (in Ltac)
    - tauto_plugin (in Tauto).
diff --git a/theories/Corelib/ssr/ssrclasses.v b/theories/Corelib/Init/ssrclasses.v
similarity index 98%
rename from theories/Corelib/ssr/ssrclasses.v
rename to theories/Corelib/Init/ssrclasses.v
index 2c31e737b66d..4b3a719e739f 100644
--- a/theories/Corelib/ssr/ssrclasses.v
+++ b/theories/Corelib/Init/ssrclasses.v
@@ -19,6 +19,8 @@
  [Require Import ssreflect] does not [Require Import RelationClasses],
  and conversely. **)
 
+Require Import Logic.
+
 Section Defs.
   Context {A : Type}.
   Class Reflexive (R : A -> A -> Prop) :=
diff --git a/theories/Corelib/ssr/ssreflect_rw.v b/theories/Corelib/Init/ssreflect_rw.v
similarity index 99%
rename from theories/Corelib/ssr/ssreflect_rw.v
rename to theories/Corelib/Init/ssreflect_rw.v
index 810e127f30ce..f697ee278e94 100644
--- a/theories/Corelib/ssr/ssreflect_rw.v
+++ b/theories/Corelib/Init/ssreflect_rw.v
@@ -12,6 +12,9 @@
 
 (** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
 
+Require Import Logic.
+Require Import Datatypes.
+Require Import Corelib.Init.Ltac.
 Require Import ssrmatching.
 Declare ML Module "rocq-runtime.plugins.ssreflect".
 
diff --git a/theories/Corelib/ssrmatching/ssrmatching.v b/theories/Corelib/Init/ssrmatching.v
similarity index 98%
rename from theories/Corelib/ssrmatching/ssrmatching.v
rename to theories/Corelib/Init/ssrmatching.v
index 617a25b1dec7..1b4ab0595c08 100644
--- a/theories/Corelib/ssrmatching/ssrmatching.v
+++ b/theories/Corelib/Init/ssrmatching.v
@@ -10,6 +10,8 @@
 
 (* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
 
+Require Import Logic.
+
 Declare ML Module "rocq-runtime.plugins.ssrmatching".
 
 Module SsrMatchingSyntax.
diff --git a/theories/Corelib/ssr/ssrunder.v b/theories/Corelib/Init/ssrunder.v
similarity index 94%
rename from theories/Corelib/ssr/ssrunder.v
rename to theories/Corelib/Init/ssrunder.v
index 49cd656bfbf7..d0cee88c1fbf 100644
--- a/theories/Corelib/ssr/ssrunder.v
+++ b/theories/Corelib/Init/ssrunder.v
@@ -19,6 +19,8 @@
  requiring [ssreflect] and use [ssreflect] without requiring [Setoid].
 *)
 
+Require Import Logic.
+Require Import Corelib.Init.Ltac.
 Require Import ssrclasses.
 
 Module Type UNDER_REL.
@@ -55,21 +57,21 @@ Definition Under_rel (A : Type) (eqA : A -> A -> Prop) :=
 Lemma Under_rel_from_rel :
   forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
     @Under_rel A eqA x y -> eqA x y.
-Proof. now trivial. Qed.
+Proof. trivial. Qed.
 Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) :
   @Under_rel A eqA = eqA.
-Proof. now trivial. Qed.
+Proof. trivial. Qed.
 Definition Over_rel := Under_rel.
 Lemma over_rel :
   forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
     @Under_rel A eqA x y = @Over_rel A eqA x y.
-Proof. now trivial. Qed.
+Proof. trivial. Qed.
 Lemma over_rel_done :
   forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Over_rel A eqA x x.
-Proof. now unfold Over_rel. Qed.
+Proof. unfold Over_rel; trivial. Qed.
 Lemma under_rel_done :
   forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
     @Under_rel A eqA x x.
-Proof. now trivial. Qed.
+Proof. trivial. Qed.
 End Under_rel.