diff --git a/clib/unicode.ml b/clib/unicode.ml
index 266059bd5e7a..6465e399de2d 100644
--- a/clib/unicode.ml
+++ b/clib/unicode.ml
@@ -122,6 +122,7 @@ let classify =
     mk_lookup_table_from_unicode_tables_for IdentSep
       [
         single 0x005F;             (* Underscore.                       *)
+        single 0x2017;             (* Double low line.                  *)
         single 0x00A0;             (* Non breaking space, overrides Sep *)
       ];
     mk_lookup_table_from_unicode_tables_for IdentPart
diff --git a/doc/Makefile.docgram b/doc/Makefile.docgram
index e78384058722..5f158279158a 100644
--- a/doc/Makefile.docgram
+++ b/doc/Makefile.docgram
@@ -38,7 +38,7 @@ REAL_DOC_MLGS := $(wildcard */*.mlg plugins/*/*.mlg)
 # omit SSR MLGS and chapter for now
 SSR_MLGS := \
 	plugins/ssr/ssrparser.mlg plugins/ssr/ssrtacs.mlg plugins/ssr/ssrvernac.mlg \
-  plugins/ssrmatching/g_ssrmatching.mlg
+  plugins/ssrmatching/g_ssrmatching.mlg plugins/ssrrewrite/ssrrewrite.mlg
 REAL_DOC_MLGS := $(filter-out $(SSR_MLGS),$(REAL_DOC_MLGS))
 SSR_RSTS := doc/sphinx/proof-engine/ssreflect-proof-language.rst
 DOC_RSTS := $(filter-out $(SSR_RSTS),$(DOC_RSTS))
diff --git a/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst
new file mode 100644
index 000000000000..82bf5fe59af0
--- /dev/null
+++ b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst
@@ -0,0 +1,12 @@
+- **Changed:**
+  ``rewrite`` tactic for ``rw``. Since this was the major cause of
+  conflict with legacy tactics, ssreflect can now be loaded with less
+  conflicts through ``From Corelib Require Import ssreflect_rw.``.
+  For backward compatibility
+  ``From Corelib Require Import ssreflect.``
+  still loads a ``rewrite`` wrapper to ``rw`` as well as the
+  ``if <term> is <pattern> then <term> else <term>``
+  and ``if <term> isn't <pattern> then <term> else <term>``
+  syntactic sugars for match
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  by Pierre Roux).
diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template
index 6923703a666c..43b5d3498687 100644
--- a/doc/corelib/index-list.html.template
+++ b/doc/corelib/index-list.html.template
@@ -113,6 +113,7 @@ through the <tt>Require Import</tt> command.</p>
   <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/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 5bb8b9770bdf..0c6366c5dd7d 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -484,7 +484,7 @@ It is used in two cases:
      constraint can be automatically discharged.
 
    + Compatibility with ssreflect's rewrite:
-     The :tacn:`rewrite (ssreflect)` tactic uses generalized rewriting when possible, by
+     The :tacn:`rw` tactic uses generalized rewriting when possible, by
      checking that a ``RewriteRelation R`` instance exists when rewriting with a
      term of type ``R t u``.
 
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 6450a6b721e3..73e7fab18dea 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -10079,7 +10079,7 @@ Changes in 8.11+beta1
   relation. More precisely, assume the given context lemma has type
   `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.  The
   first step performed by :tacn:`under` (since Coq 8.10) amounts to
-  calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which
+  calling the tactic :tacn:`rw`, which
   itself relies on :tacn:`setoid_rewrite` if need be. So this step was
   already compatible with a double implication or setoid equality for
   the conclusion head symbol `R2`. But a further step consists in
@@ -11109,7 +11109,7 @@ Many bug fixes and documentation improvements, in particular:
   by Andreas Lynge, review by Enrico Tassi)
 - Make the ``rewrite /t`` tactic work together with
   :flag:`Universe Polymorphism`.
-  This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT
+  This makes :tacn:`rw` compatible with the HoTT
   library https://github.com/HoTT/HoTT
   (`#10305 <https://github.com/rocq-prover/rocq/pull/10305>`_,
   fixes `#9336 <https://github.com/rocq-prover/rocq/issues/9336>`_,
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index f947b7a21f29..a94a6d1cdd2d 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -55,11 +55,11 @@ such as tactics to mix forward steps and generalizations as
 |SSR| adopts the point of view that rewriting, definition
 expansion and partial evaluation participate all to a same concept of
 rewriting a goal in a larger sense. As such, all these functionalities
-are provided by the :tacn:`rewrite <rewrite (ssreflect)>` tactic.
+are provided by the :tacn:`rw` tactic.
 
 |SSR| includes a little language of patterns to select subterms in
 tactics or tacticals where it matters. Its most notable application is
-in the :tacn:`rewrite <rewrite (ssreflect)>` tactic, where patterns are
+in the :tacn:`rw` tactic, where patterns are
 used to specify where the rewriting step has to take place.
 
 Finally, |SSR| supports so-called reflection steps, typically
@@ -68,8 +68,7 @@ logical view of a concept.
 
 To conclude, it is worth mentioning that |SSR| tactics can be mixed
 with non-|SSR| tactics in the same proof, or in the same Ltac
-expression. The few exceptions to this statement are described in
-section :ref:`compatibility_issues_ssr`.
+expression.
 
 
 Acknowledgments
@@ -86,9 +85,15 @@ Usage
 Getting started
 ~~~~~~~~~~~~~~~
 
-To be available, the tactics presented in this manual need the
-following minimal set of libraries to be loaded: ``ssreflect.v``,
-``ssrfun.v`` and ``ssrbool.v``.
+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
 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,
@@ -96,7 +101,7 @@ this corresponds to working in the following context:
 
 .. rocqtop:: in
 
-   From Corelib Require Import ssreflect ssrfun ssrbool.
+   From Corelib Require Import ssreflect_rw.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.
@@ -105,77 +110,6 @@ this corresponds to working in the following context:
    :flag:`Implicit Arguments`, :flag:`Strict Implicit`,
    :flag:`Printing Implicit Defensive`
 
-.. _compatibility_issues_ssr:
-
-
-Compatibility issues
-~~~~~~~~~~~~~~~~~~~~
-
-Requiring the above modules creates an environment that is mostly
-compatible with the rest of Rocq, up to a few discrepancies.
-
-
-+ New keywords (``is``) might clash with variable, constant, tactic or
-  tactical names, or with quasi-keywords in tactic or
-  notation commands.
-+ 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.
-+ Identifiers with both leading and trailing ``_``, such as ``_x_``, are
-  reserved by |SSR| and cannot appear in scripts.
-+ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those
-  available in current versions of Rocq; in particular, ``rewrite .. in
-  (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite`
-  will not work, and the |SSR| syntax and semantics for occurrence selection
-  and rule chaining are different. Use an explicit rewrite direction
-  (``rewrite <- …`` or ``rewrite -> …``) to access the Rocq rewrite tactic.
-+ New symbols (``//``, ``/=``, ``//=``) might clash with adjacent
-  existing symbols.
-  This can be avoided by inserting white spaces.
-+ New constant and theorem names might clash with the user theory.
-  This can be avoided by not importing all of |SSR|:
-
-  .. rocqtop:: in
-
-     From Corelib Require ssreflect.
-     Import ssreflect.SsrSyntax.
-
-  Note that the full
-  syntax of |SSR|’s rewrite and reserved identifiers are enabled
-  only if the ssreflect module has been required and if ``SsrSyntax`` has
-  been imported. Thus a file that requires (without importing) ``ssreflect``
-  and imports ``SsrSyntax`` can be required and imported without
-  automatically enabling |SSR|’s extended rewrite syntax and
-  reserved identifiers.
-+ 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)`.
-+ The generalization of ``if`` statements to non-Boolean conditions is turned off
-  by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the
-  ``sumXXX`` types (declared in ``ssrfun.v``) and the
-  :n:`if @term is @pattern then @term else @term` construct
-  (see :ref:`pattern_conditional_ssr`).  To use the
-  generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
-  ``Close Scope boolean_if_scope``.
-+ The following flags can be unset to make |SSR| more compatible with
-  parts of Rocq.
-
-.. flag:: SsrRewrite
-
-   Controls whether the incompatible rewrite syntax is enabled (the default).
-   Disabling the :term:`flag` makes the syntax compatible with other parts of Rocq.
-
-.. flag:: SsrIdents
-
-   Controls whether tactics can refer to |SSR|-generated variables that are
-   in the form _xxx_.  Scripts with explicit references to such variables
-   are fragile; they are prone to failure if the proof is later modified or
-   if the details of variable name generation change in future releases of Rocq.
-
-   The default is on, which gives an error message when the user tries to
-   create such identifiers.  Disabling the :term:`flag` generates a warning instead,
-   increasing compatibility with other parts of Rocq.
-
 Gallina extensions
 --------------------
 
@@ -217,7 +151,7 @@ construct differs from the latter as follows.
 
     .. rocqtop:: reset none
 
-       From Corelib Require Import ssreflect.
+       From Corelib Require Import ssreflect_rw.
        Set Implicit Arguments.
        Unset Strict Implicit.
        Unset Printing Implicit Defensive.
@@ -257,7 +191,8 @@ dependent pattern matching and for aliasing the pattern (see
 Pattern conditional
 ~~~~~~~~~~~~~~~~~~~
 
-The following construct can be used for a refutable pattern matching,
+When doing ``From Corelib Require Import ssreflect`` (not ``ssreflect_rw``),
+the following construct can be used for a refutable pattern matching,
 that is, pattern testing:
 
 .. prodn::
@@ -275,15 +210,16 @@ example, the null and all list function(al)s can be defined as follows:
 
     .. rocqtop:: reset none
 
-       From Corelib Require Import ssreflect.
        Set Implicit Arguments.
        Unset Strict Implicit.
        Unset Printing Implicit Defensive.
-       Section Test.
 
    .. rocqtop:: all
 
-      Variable d: Set.
+      From Corelib Require Import ssreflect.
+
+      Section Test.
+      Variable d : Set.
       Definition null (s : list d) :=
         if s is nil then true else false.
       Variable a : d -> bool.
@@ -311,13 +247,15 @@ The latter appears to be marginally shorter, but it is quite
 ambiguous, and indeed often requires an explicit annotation
 ``(term : {_} + {_})`` to type check, which evens the character count.
 
-Therefore, |SSR| restricts by default the condition of a plain ``if``
+Therefore, ``From Corelib Require Import ssreflect`` restricts by default the condition of a plain ``if``
 construct to the standard ``bool`` type; this avoids spurious type
 annotations.
 
 .. example::
 
-   .. rocqtop:: all
+   .. rocqtop:: reset all
+
+      From Corelib Require Import ssreflect.
 
       Definition orb b1 b2 := if b1 then true else b2.
 
@@ -376,7 +314,7 @@ expressions such as
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -401,7 +339,7 @@ each point of use; e.g., the above definition can be written:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -446,16 +384,12 @@ Anonymous arguments
 
 When in a definition, the type of a certain argument is mandatory, but
 not its name, one usually uses “arrow” abstractions for prenex
-arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|,
-the latter can be replaced by the open syntax ``of term`` or
-(equivalently) ``& term``, which are both syntactically equivalent to a
-``(_ : term)`` expression. This feature almost behaves as the
-following extension of the binder syntax:
-
-.. prodn::
-   binder += {| & @term | of @term }
+arguments, or the ``(_ : term)`` syntax for inner arguments.
+The latter can be replaced by the open syntax ``& term``,
+which is syntactically equivalent to a
+``(_ : term)`` expression.
 
-Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end
+Caveat: ``& T`` abbreviations have to appear at the end
 of a binder list. For instance, the usual two-constructor polymorphic
 type list, i.e., the one of the standard ``List`` library, can be
 defined by the following declaration:
@@ -464,14 +398,13 @@ defined by the following declaration:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
 
   .. rocqtop:: all
 
-     Inductive list (A : Type) : Type := nil | cons of A & list A.
+     Inductive list (A : Type) : Type := nil | cons & A & list A.
 
 
 Wildcards
@@ -518,7 +451,7 @@ For example, the tactic :tacn:`pose (ssreflect)` supports parameters:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -633,7 +566,7 @@ where:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -681,7 +614,7 @@ conditions.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -702,7 +635,7 @@ conditions.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -723,7 +656,7 @@ Moreover:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -743,7 +676,7 @@ Moreover:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -776,7 +709,7 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -798,7 +731,7 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -819,7 +752,7 @@ An *occurrence switch* can be:
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -850,7 +783,7 @@ selection.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -867,7 +800,7 @@ only one occurrence of the selected term.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -898,7 +831,7 @@ context of a goal thanks to the ``in`` tactical.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
 
      .. rocqtop:: all
 
@@ -914,7 +847,7 @@ context of a goal thanks to the ``in`` tactical.
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
 
      .. rocqtop:: all
 
@@ -1030,7 +963,7 @@ constants to the goal.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1091,7 +1024,7 @@ The ``:`` tactical is used to operate on an element in the context.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -1186,7 +1119,7 @@ The move tactic.
 
       .. rocqtop:: reset all
 
-         Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Goal not False.
          move.
 
@@ -1256,7 +1189,7 @@ The elim tactic
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -1296,7 +1229,7 @@ existential metavariables of sort :g:`Prop`.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1443,7 +1376,7 @@ If the tactic is ``move`` or ``case`` and an equation :token:`ident` is given, t
 (step 3) for :token:`d_item` is suppressed (see Section :ref:`generation_of_equations_ssr`).
 
 Intro patterns (see Section :ref:`introduction_ssr`)
-and the ``rewrite`` tactic (see Section :ref:`rewriting_ssr`)
+and the ``rw`` tactic (see Section :ref:`rewriting_ssr`)
 let one place a :token:`clear_switch` in the middle of other items
 (namely identifiers, views and rewrite rules).  This can trigger the
 addition of proof context items to the ones being explicitly
@@ -1476,7 +1409,7 @@ context to interpret wildcards; in particular, it can accommodate the
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1714,7 +1647,7 @@ Intro patterns
   (resp. :token:`occ_switch` ``<-``)
   pops the top assumption (which should be a rewritable proposition) into an
   anonymous fact, rewrites (resp. rewrites right to left) the goal with this
-  fact (using the |SSR| ``rewrite`` tactic described in Section
+  fact (using the |SSR| ``rw`` tactic described in Section
   :ref:`rewriting_ssr`, and honoring the optional occurrence selector), and
   finally deletes the anonymous fact from the context.
 ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]``
@@ -1768,13 +1701,15 @@ Clears are deferred until the end of the intro pattern.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect ssrbool.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
 
    .. rocqtop:: all
 
+      From Corelib Require Import ssrbool.
+
       Lemma test x y : Nat.leb 0 x = true -> (Nat.leb 0 x) && (Nat.leb y 2) = true.
       move=> {x} ->.
 
@@ -1829,7 +1764,7 @@ Block introduction
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -1882,7 +1817,7 @@ deal with the possible parameters of the constants introduced.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1901,7 +1836,7 @@ under fresh |SSR| names.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -1968,7 +1903,7 @@ be substituted.
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
@@ -2074,20 +2009,20 @@ of the time more than two levels of indentation.
 Here is a fragment of such a structured script::
 
     case E1: (abezoutn _ _) => [[| k1] [| k2]].
-    - rewrite !muln0 !gexpn0 mulg1 => H1.
-      move/eqP: (sym_equal F0); rewrite -H1 orderg1 eqn_mul1.
+    - rw !muln0 !gexpn0 mulg1 => H1.
+      move/eqP: (sym_equal F0); rw -H1 orderg1 eqn_mul1.
       by case/andP; move/eqP.
-    - rewrite muln0 gexpn0 mulg1 => H1.
+    - rw muln0 gexpn0 mulg1 => H1.
       have F1: t %| t * S k2.+1 - 1.
-        apply: (@dvdn_trans (orderg x)); first by rewrite F0; exact: dvdn_mull.
-        rewrite orderg_dvd; apply/eqP; apply: (mulgI x).
-        rewrite -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //.
+        apply: (@dvdn_trans (orderg x)); first by rw F0; exact: dvdn_mull.
+        rw orderg_dvd; apply/eqP; apply: (mulgI x).
+        rw -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //.
         by move: P1; case t.
-      rewrite dvdn_subr in F1; last by exact: dvdn_mulr.
-      + rewrite H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _).
-        by apply/eqP; rewrite -dvdn1.
+      rw dvdn_subr in F1; last by exact: dvdn_mulr.
+      + rw H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _).
+        by apply/eqP; rw -dvdn1.
       + by move: P1; case: (t) => [| [| s1]].
-    - rewrite muln0 gexpn0 mul1g => H1.
+    - rw muln0 gexpn0 mul1g => H1.
     ...
 
 
@@ -2122,7 +2057,7 @@ with a ``by``, like in:
 
 .. rocqdoc::
 
-   by apply/eqP; rewrite -dvdn1.
+   by apply/eqP; rw -dvdn1.
 
 .. tacn:: done
    :name: done
@@ -2141,7 +2076,7 @@ with a ``by``, like in:
 
       Ltac done :=
         trivial; hnf; intros; solve
-         [ do ![solve [trivial | apply: sym_equal; trivial]
+         [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial]
                | discriminate | contradiction | split]
          | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
@@ -2187,19 +2122,19 @@ is equivalent to:
 
    .. rocqdoc::
 
-      by rewrite my_lemma1.
+      by rw my_lemma1.
 
    succeeds, then the tactic:
 
    .. rocqdoc::
 
-      by rewrite my_lemma1; apply my_lemma2.
+      by rw my_lemma1; apply my_lemma2.
 
    usually fails since it is equivalent to:
 
    .. rocqdoc::
 
-      by (rewrite my_lemma1; apply my_lemma2).
+      by (rw my_lemma1; apply my_lemma2).
 
 
 .. _selectors_ssr:
@@ -2269,7 +2204,7 @@ to the others.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -2335,14 +2270,14 @@ For instance, the tactic:
 
 .. rocqdoc::
 
-   tactic; do 1? rewrite mult_comm.
+   tactic; do 1? rw mult_comm.
 
 rewrites at most one time the lemma ``mult_comm`` in all the subgoals
 generated by tactic, whereas the tactic:
 
 .. rocqdoc::
 
-   tactic; do 2! rewrite mult_comm.
+   tactic; do 2! rw mult_comm.
 
 rewrites exactly two times the lemma ``mult_comm`` in all the subgoals
 generated by ``tactic``, and fails if this rewrite is not possible in some
@@ -2367,7 +2302,7 @@ already presented the *localization* tactical ``in``, whose general syntax is:
 
 where :token:`ident` is a name in the
 context. On the left side of ``in``,
-:token:`tactic` can be ``move``, ``case``, ``elim``, ``rewrite``, ``set``,
+:token:`tactic` can be ``move``, ``case``, ``elim``, ``rw``, ``set``,
 or any tactic formed with the general iteration tactical ``do`` (see Section
 :ref:`iteration_ssr`).
 
@@ -2388,14 +2323,14 @@ between standard Ltac ``in`` and the |SSR| tactical in.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
 
   .. rocqtop:: all
 
-     Ltac mytac H := rewrite H.
+     Ltac mytac H := rw H.
 
      Lemma test x y (H1 : x = y) (H2 : y = 3) : x + y = 6.
      do [mytac H2] in H1 *.
@@ -2406,7 +2341,7 @@ between standard Ltac ``in`` and the |SSR| tactical in.
 By default, ``in`` keeps the body of local definitions. To erase the body
 of a local definition during the generalization phase, the name of the
 local definition must be written between parentheses, like in
-``rewrite H in H1 (def_n) H2.``
+``rw H in H1 (def_n) H2.``
 
 .. tacv:: @tactic in {+ {| @clear_switch | {? @}@ident | ( @ident ) | ( {? @}@ident := @c_pattern ) } } {? * }
 
@@ -2463,7 +2398,7 @@ the holes are abstracted in term.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2477,7 +2412,7 @@ the holes are abstracted in term.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2495,7 +2430,7 @@ tactic:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2539,7 +2474,7 @@ statement is very short, basically when it fits in one line like in:
 
 .. rocqdoc::
 
-   have H23 : 3 + 2 = 2 + 3 by rewrite addnC.
+   have H23 : 3 + 2 = 2 + 3 by rw addnC.
 
 The possibility of using :token:`i_item` supplies a very concise syntax for
 the further use of the intermediate step. For instance,
@@ -2548,7 +2483,7 @@ the further use of the intermediate step. For instance,
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2576,7 +2511,7 @@ destruction of existential assumptions like in the tactic:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2603,7 +2538,7 @@ term for the intermediate lemma, using tactics of the form:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2623,16 +2558,18 @@ The following example requires the mathcomp and mczify libraries.
 
 .. example::
 
-  .. rocqtop:: reset none warn extra-mathcomp extra-mczify
-
-     From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat zify.
+  .. rocqtop:: reset none
 
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
+     Set Warnings "-notation-overridden".
 
   .. rocqtop:: all extra-mathcomp extra-mczify
 
+     From Corelib Require Import ssreflect_rw.
+     From mathcomp Require Import ssrfun ssrbool ssrnat zify.
+
      Lemma test : True.
      have H x (y : nat) : 2 * x + y = x + x + y by lia.
 
@@ -2745,7 +2682,7 @@ typeclass inference.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
 
      Axiom ty : Type.
      Axiom t : ty.
@@ -2890,16 +2827,19 @@ simplifies a proof. Here is an example showing the beginning of the
 proof that quotient and reminder of natural number euclidean division
 are unique.
 
-The following example requires the mathcomp and mczify libraries.
+The following example requires the mathcomp library.
 
 .. example::
 
-  .. rocqtop:: reset none warn extra-mathcomp
+  .. rocqtop:: reset none
 
-     From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat.
+     Set Warnings "-notation-overridden".
 
   .. 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 :
        q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2).
      wlog: q1 q2 r1 r2 / q1 <= q2.
@@ -2921,7 +2861,7 @@ pattern will be used to process its instance.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrfun ssrbool.
+     From Corelib Require Import ssreflect_rw ssrfun ssrbool.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2971,7 +2911,7 @@ illustrated in the following example.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2990,7 +2930,7 @@ illustrated in the following example.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3015,7 +2955,7 @@ intermediate results handled are properties of effectively computable
 functions. The most efficient means of establishing such results are
 computation and simplification of expressions involving such
 functions, i.e., rewriting. |SSR| therefore includes an
-extended ``rewrite`` tactic that unifies and combines most of the
+extended ``rw`` tactic that unifies and combines most of the
 rewriting functionalities.
 
 
@@ -3034,8 +2974,7 @@ The main features of the rewrite tactic are:
 
 The general form of an |SSR| rewrite tactic is:
 
-.. tacn:: rewrite {+ @rstep }
-   :name: rewrite (ssreflect)
+.. tacn:: rw {+ @rstep }
    :undocumented:
 
 The combination of a rewrite tactic with the ``in`` tactical (see Section
@@ -3085,7 +3024,7 @@ operation should be performed.
   :token:`r_item` is actually processed and is complemented with the name of
   the rewrite rule if and only if it is a simple proof context entry [#10]_.
   As a consequence, one can
-  write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately
+  write ``rw {}H`` to rewrite with ``H`` and dispose ``H`` immediately
   afterwards.
   This behavior can be avoided by putting parentheses around the rewrite rule.
 
@@ -3097,16 +3036,16 @@ A :token:`r_item` can be one of the following.
   :ref:`introduction_ssr`). Simplification operations are intertwined with the possible
   other rewrite operations specified by the list of :token:`r_item`.
 + A *folding/unfolding* :token:`r_item`. The tactic
-  ``rewrite /term`` unfolds the
+  ``rw /term`` unfolds the
   :term:`head constant` of ``term`` in every occurrence of the first matching of
   ``term`` in the goal. In particular, if ``my_def`` is a (local or global)
-  defined constant, the tactic ``rewrite /my_def.`` is analogous to:
+  defined constant, the tactic ``rw /my_def.`` is analogous to:
   ``unfold my_def``.
-  Conversely, ``rewrite -/my_def.`` is equivalent to ``fold my_def``.
+  Conversely, ``rw -/my_def.`` is equivalent to ``fold my_def``.
   When an unfold :token:`r_item` is combined with a
   redex pattern, a conversion
   operation is performed. A tactic of the form
-  ``rewrite -[term1]/term2.``
+  ``rw -[term1]/term2.``
   is equivalent to ``change term1 with term2.`` If ``term2`` is a
   single constant and ``term1`` head symbol is not ``term2``, then the head
   symbol of ``term1`` is repeatedly unfolded until ``term2`` appears.
@@ -3116,15 +3055,15 @@ A :token:`r_item` can be one of the following.
       ``eq`` is the Leibniz equality or a registered setoid
       equality;
     + a list of terms ``(t1 ,…,tn)``, each ``ti`` having a type as above, and
-      the tactic ``rewrite r_prefix (t1 ,…,tn ).``
-      is equivalent to ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``;
+      the tactic ``rw r_prefix (t1 ,…,tn ).``
+      is equivalent to ``do [rw r_prefix t1 | … | rw r_prefix tn ].``;
     + an anonymous rewrite lemma ``(_ : term)``, where ``term`` has a type as above.
 
   .. example::
 
      .. rocqtop:: reset none
 
-        From Corelib Require Import ssreflect.
+        From Corelib Require Import ssreflect_rw.
         Set Implicit Arguments.
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
@@ -3134,7 +3073,7 @@ A :token:`r_item` can be one of the following.
         Definition double x := x + x.
         Definition ddouble x := double (double x).
         Lemma test x : ddouble x = 4 * x.
-        rewrite [ddouble _]/double.
+        rw [ddouble _]/double.
 
   .. warning::
 
@@ -3148,13 +3087,13 @@ A :token:`r_item` can be one of the following.
 
      .. rocqtop:: all fail
 
-        rewrite -[f y]/(y + _).
+        rw -[f y]/(y + _).
 
      but the following script succeeds
 
      .. rocqtop:: all
 
-        rewrite -[f y x]/(y + _).
+        rw -[f y x]/(y + _).
 
 
 .. flag:: SsrOldRewriteGoalsOrder
@@ -3185,7 +3124,7 @@ In a rewrite tactic of the form:
 
 .. rocqdoc::
 
-   rewrite occ_switch [term1]term2.
+   rw occ_switch [term1]term2.
 
 ``term1`` is the explicit rewrite redex and ``term2`` is the rewrite rule.
 This execution of this tactic unfolds as follows.
@@ -3228,7 +3167,7 @@ tactic:
 
 .. rocqdoc::
 
-   rewrite /my_def {2}[f _]/= my_eq //=.
+   rw /my_def {2}[f _]/= my_eq //=.
 
 
 unfolds ``my_def`` in the goal, simplifies the second occurrence of the
@@ -3243,7 +3182,7 @@ proof of basic results on natural numbers arithmetic.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3255,11 +3194,11 @@ proof of basic results on natural numbers arithmetic.
      Axiom addSnnS : forall m n, S m + n = m + S n.
 
      Lemma addnCA m n p : m + (n + p) = n + (m + p).
-     by elim: m p => [ | m Hrec] p; rewrite ?addSnnS -?addnS.
+     by elim: m p => [ | m Hrec] p; rw ?addSnnS -?addnS.
      Qed.
 
      Lemma addnC n m : m + n = n + m.
-     by rewrite -{1}[n]addn0 addnCA addn0.
+     by rw -{1}[n]addn0 addnCA addn0.
      Qed.
 
 Note the use of the ``?`` switch for parallel rewrite operations in the
@@ -3279,7 +3218,7 @@ side of the equality the user wants to rewrite.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3287,7 +3226,7 @@ side of the equality the user wants to rewrite.
   .. rocqtop:: all
 
      Lemma test (H : forall t u, t + u = u + t) x y : x + y = y + x.
-     rewrite [y + _]H.
+     rw [y + _]H.
 
 Note that if this first pattern matching is not compatible with the
 :token:`r_item`, the rewrite fails, even if the goal contains a
@@ -3299,7 +3238,7 @@ the equality.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3307,7 +3246,7 @@ the equality.
   .. rocqtop:: all
 
      Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0.
-     Fail rewrite [x + _]H.
+     Fail rw [x + _]H.
 
   Indeed, the left-hand side of ``H`` does not match
   the redex identified by the pattern ``x + y * 4``.
@@ -3322,7 +3261,7 @@ Occurrence switches and redex switches
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3330,7 +3269,7 @@ Occurrence switches and redex switches
   .. rocqtop:: all
 
      Lemma test x y : x + y + 0 = x + y + y + 0 + 0 + (x + y + 0).
-     rewrite {2}[_ + y + 0](_: forall z, z + 0 = z).
+     rw {2}[_ + y + 0](_: forall z, z + 0 = z).
 
 The second subgoal is generated by the use of an anonymous lemma in
 the rewrite tactic. The effect of the tactic on the initial goal is to
@@ -3351,7 +3290,7 @@ repetition.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3359,7 +3298,7 @@ repetition.
   .. rocqtop:: all
 
      Lemma test x y (z : nat) : x + 1 = x + y + 1.
-     rewrite 2!(_ : _ + 1 = z).
+     rw 2!(_ : _ + 1 = z).
 
 This last tactic generates *three* subgoals because
 the second rewrite operation specified with the ``2!`` multiplier
@@ -3381,7 +3320,7 @@ rewrite operations prescribed by the rules on the current goal.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3395,7 +3334,7 @@ rewrite operations prescribed by the rules on the current goal.
      Hypothesis eqac : a = c.
 
      Lemma test : a = a.
-     rewrite (eqab, eqac).
+     rw (eqab, eqac).
 
   Indeed, rule ``eqab`` is the first to apply among the ones
   gathered in the tuple passed to the rewrite tactic. This multirule
@@ -3406,8 +3345,8 @@ rewrite operations prescribed by the rules on the current goal.
 
      Definition multi1 := (eqab, eqac).
 
-  In this case, the tactic ``rewrite multi1`` is a synonym for
-  ``rewrite (eqab, eqac)``.
+  In this case, the tactic ``rw multi1`` is a synonym for
+  ``rw (eqab, eqac)``.
 
 More precisely, a multirule rewrites the first subterm to which one of
 the rules applies in a left-to-right traversal of the goal, with the
@@ -3425,7 +3364,7 @@ literal matches have priority.
       Definition multi2 := (eqab, eqd0).
 
       Lemma test : d = b.
-      rewrite multi2.
+      rw multi2.
 
    Indeed, rule ``eqd0`` applies without unfolding the
    definition of ``d``.
@@ -3443,7 +3382,7 @@ repeated anew.
      Definition multi3 := (eq_adda_b, eq_adda_c, eqb0).
 
      Lemma test : 1 + a = 12 + a.
-     rewrite 2!multi3.
+     rw 2!multi3.
 
   It uses ``eq_adda_b`` then ``eqb0`` on the left-hand
   side only. Without the bound ``2``, one would obtain ``0 = 0``.
@@ -3454,7 +3393,7 @@ to (universally) quantify over the parameters of a subset of rules (as
 there is special code that will omit unnecessary quantifiers for rules
 that can be syntactically extracted). It is also possible to reverse
 the direction of a rule subset, using a special dedicated syntax: the
-tactic rewrite ``(=^~ multi1)`` is equivalent to ``rewrite multi1_rev``.
+tactic rewrite ``(=^~ multi1)`` is equivalent to ``rw multi1_rev``.
 
 .. example::
 
@@ -3497,7 +3436,7 @@ the efficient operations, we gather all these rules in the definition
 
    Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
 
-The tactic ``rewrite !trecE.``
+The tactic ``rw !trecE.``
 restores the naive version of each operation in a goal involving the
 efficient ones, e.g., for the purpose of a correctness proof.
 
@@ -3506,16 +3445,16 @@ Wildcards vs abstractions
 `````````````````````````
 
 The rewrite tactic supports :token:`r_item`\s containing holes. For example, in
-the tactic ``rewrite (_ : _ * 0 = 0).``,
+the tactic ``rw (_ : _ * 0 = 0).``,
 the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.``
 Anyway this tactic is *not* equivalent to
-``rewrite (_ : forall x, x * 0 = 0).``.
+``rw (_ : forall x, x * 0 = 0).``.
 
 .. example::
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3525,13 +3464,13 @@ Anyway this tactic is *not* equivalent to
   .. rocqtop:: all
 
      Lemma test y z : y * 0 + y * (z * 0) = 0.
-     rewrite (_ : _ * 0 = 0).
+     rw (_ : _ * 0 = 0).
 
   while the other tactic results in
 
   .. rocqtop:: all restart abort
 
-     rewrite (_ : forall x, x * 0 = 0).
+     rw (_ : forall x, x * 0 = 0).
 
   The first tactic requires you to prove the instance of the (missing)
   lemma that was used, while the latter requires you prove the quantified
@@ -3565,7 +3504,7 @@ cases.
 
     .. rocqtop:: reset none
 
-       From Corelib Require Import ssreflect.
+       From Corelib Require Import ssreflect_rw.
        Set Implicit Arguments.
        Unset Strict Implicit.
        Unset Printing Implicit Defensive.
@@ -3580,7 +3519,7 @@ cases.
 
        Lemma test : f 3 + f 3 = f 6.
        (* we call the standard rewrite tactic here *)
-       rewrite -> H.
+       rewrite H.
 
     This rewriting is not possible in |SSR|, because
     there is no occurrence of the head symbol ``f`` of the rewrite rule in the
@@ -3588,23 +3527,23 @@ cases.
 
     .. rocqtop:: all restart fail
 
-       rewrite H.
+       rw H.
 
     Rewriting with ``H`` first requires unfolding the occurrences of
     ``f``
     where the substitution is to be performed (here there is a single such
-    occurrence), using tactic ``rewrite /f`` (for a global replacement of
-    ``f`` by ``g``) or ``rewrite pattern/f``, for a finer selection.
+    occurrence), using tactic ``rw /f`` (for a global replacement of
+    ``f`` by ``g``) or ``rw pattern/f``, for a finer selection.
 
     .. rocqtop:: all restart
 
-       rewrite /f H.
+       rw /f H.
 
     Alternatively, one can override the pattern inferred from ``H``
 
     .. rocqtop:: all restart
 
-       rewrite [f _]H.
+       rw [f _]H.
 
 
 Existential metavariables and rewriting
@@ -3623,7 +3562,6 @@ corresponding new goals will be generated.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrfun ssrbool.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -3631,6 +3569,8 @@ corresponding new goals will be generated.
 
   .. rocqtop:: all abort
 
+     From Corelib Require Import ssreflect ssrfun ssrbool.
+
      Axiom leq : nat -> nat -> bool.
      Notation "m <= n" := (leq m n) : nat_scope.
      Notation "m < n"  := (S m <= n) : nat_scope.
@@ -3643,11 +3583,11 @@ corresponding new goals will be generated.
      Axiom insubT : forall n x Px, insub n x = Some (Sub x Px).
 
      Lemma test (x : 'I_2) y : Some x = insub 2 y.
-     rewrite insubT.
+     rw insubT.
 
   Since the argument corresponding to ``Px`` is not supplied by the user, the
   resulting goal should be ``Some x = Some (Sub y ?Goal).``
-  Instead, |SSR| ``rewrite`` tactic hides the existential variable.
+  Instead, |SSR| ``rw`` tactic hides the existential variable.
 
   As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to
   solve the existential variable.
@@ -3655,7 +3595,7 @@ corresponding new goals will be generated.
   .. rocqtop:: all abort
 
      Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y.
-     rewrite insubT.
+     rw insubT.
 
 
 As a temporary limitation, this behavior is available only if the
@@ -3680,7 +3620,7 @@ complete terms, as shown by the simple example below.
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -3703,7 +3643,7 @@ complete terms, as shown by the simple example below.
 
    .. rocqtop:: all fail
 
-      rewrite eq_map.
+      rw eq_map.
 
    as we need to explicitly provide the non-inferable argument ``F2``,
    which corresponds here to the term we want to obtain *after* the
@@ -3712,8 +3652,8 @@ complete terms, as shown by the simple example below.
 
    .. rocqtop:: all abort
 
-      rewrite (@eq_map _ (fun _ : nat => 0)).
-        by move=> m; rewrite subnn.
+      rw (@eq_map _ (fun _ : nat => 0)).
+        by move=> m; rw subnn.
 
    The :tacn:`under` tactic lets one perform the same operation in a more
    convenient way:
@@ -3721,7 +3661,7 @@ complete terms, as shown by the simple example below.
    .. rocqtop:: all abort
 
       Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
-      under eq_map => m do rewrite subnn.
+      under eq_map => m do rw subnn.
 
 
 The under tactic
@@ -3759,7 +3699,7 @@ Let us redo the running example in interactive mode.
 
       Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
       under eq_map => m.
-        rewrite subnn.
+        rw subnn.
         over.
 
 The execution of the Ltac expression:
@@ -3768,8 +3708,8 @@ The execution of the Ltac expression:
 
 involves the following steps.
 
-1. It performs a :n:`rewrite @term`
-   without failing like in the first example with ``rewrite eq_map.``,
+1. It performs a :n:`rw @term`
+   without failing like in the first example with ``rw eq_map.``,
    but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
    a pattern or an occurrence selector, then the modifiers are honoured.
 
@@ -3787,7 +3727,8 @@ 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 ``Require Import ssreflect.`` and ``Require Setoid.``)
+   both ``From Corelib Require Import ssreflect_rw.``
+   and ``From Corelib Require Setoid.``)
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
@@ -3871,7 +3812,7 @@ Notes:
 
    .. rocqtop:: reset none
 
-      From Corelib Require Import ssreflect.
+      From Corelib Require Import ssreflect_rw.
       Set Implicit Arguments.
       Unset Strict Implicit.
       Unset Printing Implicit Defensive.
@@ -3935,7 +3876,7 @@ Notes:
         \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i).
       under eq_bigr => i prime_i do
         under eq_big => [ j | j odd_j ] do
-          [ rewrite (muln1 j) | rewrite (addnC i j) ].
+          [ rw (muln1 j) | rw (addnC i j) ].
 
    Remark how the final goal uses the name ``i`` (the name given in the
    intro pattern) rather than ``a`` in the binder of the first summation.
@@ -3978,21 +3919,22 @@ selective rewriting, blocking on the fly the reduction in the term ``t``.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrfun ssrbool.
-     From Corelib Require Import ListDef.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssreflect ssrfun ssrbool.
+     From Corelib Require Import ListDef.
+     Section Test.
+
      Variable A : Type.
      Fixpoint has (p : A -> bool) (l : list A) : bool :=
        if l is cons x l then p x || (has p l) else false.
 
      Lemma test p x y l (H : p x = true) : has p ( x :: y :: l) = true.
-     rewrite {2}[cons]lock /= -lock.
+     rw {2}[cons]lock /= -lock.
 
 It is sometimes desirable to globally prevent a definition from being
 expanded by simplification; this is done by adding ``locked`` in the
@@ -4002,7 +3944,7 @@ definition.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4013,7 +3955,7 @@ definition.
       Definition lid := locked (fun x : nat => x).
 
       Lemma test : lid 3 = 3.
-      rewrite /=.
+      rw /=.
       unlock lid.
 
 .. tacn:: unlock {? @occ_switch } @ident
@@ -4073,7 +4015,7 @@ arithmetic operations. We define for instance:
 The operation ``addn`` behaves exactly like ``plus``, except that
 ``(addn (S n) m)`` will not simplify spontaneously to
 ``(S (addn n m))`` (the two terms, however, are convertible).
-In addition, the unfolding step ``rewrite /addn``
+In addition, the unfolding step ``rw /addn``
 will replace ``addn`` directly with ``plus``, so the ``nosimpl`` form is
 essentially invisible.
 
@@ -4115,11 +4057,10 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
-         Section Test.
 
       .. rocqtop:: all
 
@@ -4142,14 +4083,14 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
-         Section Test.
 
       .. rocqtop:: all
 
+         From Corelib Require Import ssreflect.
+
          Definition f n :=
            if n is 0 then plus else mult.
          Definition g (n m : nat) := plus.
@@ -4165,18 +4106,17 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
-         Section Test.
 
       .. rocqtop:: all
 
          Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n.
-         congr S; rewrite -/plus.
+         congr S; rw -/plus.
 
-      The tactic ``rewrite -/plus`` folds back the expansion of ``plus``,
+      The tactic ``rw -/plus`` folds back the expansion of ``plus``,
       which was necessary for matching both sides of the equality with
       an application of ``S``.
 
@@ -4186,11 +4126,10 @@ which the function is supplied:
 
       .. rocqtop:: reset none
 
-         From Corelib Require Import ssreflect.
+         From Corelib Require Import ssreflect_rw.
          Set Implicit Arguments.
          Unset Strict Implicit.
          Unset Printing Implicit Defensive.
-         Section Test.
 
       .. rocqtop:: all
 
@@ -4253,7 +4192,7 @@ in the second column.
 
 The rewrite tactic supports two more patterns obtained prefixing the
 first two with ``in``. The intended meaning is that the pattern identifies
-all subterms of the specified context. The ``rewrite`` tactic will infer a
+all subterms of the specified context. The ``rw`` tactic will infer a
 pattern for the redex looking at the rule used for rewriting.
 
 .. list-table::
@@ -4287,11 +4226,11 @@ consider the goal ``a = b`` and the tactic
 
 .. rocqdoc::
 
-   rewrite [in X in _ = X]rule.
+   rw [in X in _ = X]rule.
 
 It rewrites all occurrences of the left hand side of ``rule``
 inside ``b``  only (``a``, and the hidden type of the equality, are ignored). Note that the
-variant ``rewrite [X in _ = X]rule`` would have rewritten ``b``
+variant ``rw [X in _ = X]rule`` would have rewritten ``b``
 exactly (i.e., it would only work if ``b`` and the left-hand side
 of rule can be unified).
 
@@ -4366,17 +4305,16 @@ parentheses are required around more complex patterns.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
      Lemma test a b : a + b + 1 = b + (a + 1).
      set t := (X in _ = X).
-     rewrite {}/t.
+     rw {}/t.
      set t := (a + _ in X in _ = X).
 
 
@@ -4405,11 +4343,10 @@ Contextual patterns in rewrite
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
@@ -4421,7 +4358,7 @@ Contextual patterns in rewrite
      Axiom addnC : forall m n, m + n = n + m.
 
      Lemma test x y z f : (x.+1 + y) + f (x.+1 + y) (z + (x + y).+1) = 0.
-     rewrite [in f _ _]addSn.
+     rw [in f _ _]addSn.
 
   Note: the simplification rule ``addSn`` is applied only under the ``f``
   symbol.
@@ -4429,7 +4366,7 @@ Contextual patterns in rewrite
 
   .. rocqtop:: all
 
-     rewrite addSn -[X in _ = X]addn0.
+     rw addSn -[X in _ = X]addn0.
 
   Note that the right-hand side of ``addn0`` is undetermined, but the
   rewrite pattern specifies the redex explicitly. The right-hand side
@@ -4442,13 +4379,13 @@ Contextual patterns in rewrite
 
   .. rocqtop:: all
 
-     rewrite -{2}[in X in _ = X](addn0 0).
+     rw -{2}[in X in _ = X](addn0 0).
 
   The following tactic is quite tricky:
 
   .. rocqtop:: all
 
-     rewrite [_.+1 in X in f _ X](addnC x.+1).
+     rw [_.+1 in X in f _ X](addnC x.+1).
 
   The explicit redex ``_.+1`` is important, since its :term:`head constant` ``S``
   differs from the head constant inferred from
@@ -4468,7 +4405,7 @@ Contextual patterns in rewrite
 
   .. rocqtop:: all
 
-     rewrite [x.+1 + y as X in f X _]addnC.
+     rw [x.+1 + y as X in f X _]addnC.
 
 
 Patterns for recurrent contexts
@@ -4495,7 +4432,7 @@ Shortcuts defined this way can be freely used in place of the trailing
 .. rocqdoc::
 
    set rhs := RHS.
-   rewrite [in RHS]rule.
+   rw [in RHS]rule.
    case: (a + _ in RHS).
 
 
@@ -4569,14 +4506,15 @@ generation (see Section :ref:`generation_of_equations_ssr`).
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ListDef.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssreflect ListDef.
+     Section Test.
+
      Variable d : Type.
      Fixpoint add_last (s : list d) (z : d) {struct s} : list d :=
        if s is cons x s' then cons x (add_last s' z) else z :: nil.
@@ -4644,7 +4582,7 @@ Here is an example of a regular, but nontrivial, eliminator.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4658,10 +4596,10 @@ Here is an example of a regular, but nontrivial, eliminator.
                                      end -> P _x m) -> forall n : nat, P n (plus m n).
      Admitted.
 
-     Section Test.
-
   .. rocqtop:: all
 
+     From Corelib Require Import ssreflect.
+
      Fixpoint plus (m n : nat) {struct n} : nat :=
        if n is S p then S (plus m p) else m.
 
@@ -4682,10 +4620,10 @@ Here is an example of a regular, but nontrivial, eliminator.
   .. rocqtop:: reset none
 
      From Corelib Require Import ssreflect.
+
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
      Fixpoint plus (m n : nat) {struct n} : nat :=
        if n is S p then S (plus m p) else m.
@@ -4713,6 +4651,7 @@ Here is an example of a regular, but nontrivial, eliminator.
   .. rocqtop:: reset none
 
      From Corelib Require Import ssreflect.
+
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4748,11 +4687,10 @@ Here is an example of a truncated eliminator:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqdoc::
 
@@ -4812,7 +4750,7 @@ disjunction.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4833,7 +4771,7 @@ disjunction.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4868,7 +4806,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4901,7 +4839,7 @@ relevant for the current goal.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -4945,11 +4883,10 @@ assumption to some given arguments.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
@@ -4974,14 +4911,16 @@ bookkeeping steps.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+     Section Test.
+
      Variables P Q: bool -> Prop.
      Hypothesis PQequiv : forall a b, P (a || b) <-> Q a.
 
@@ -5030,7 +4969,7 @@ analysis:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5047,14 +4986,15 @@ analysis
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+
      Lemma test b : b || ~~ b = true.
      by case: b.
 
@@ -5137,7 +5077,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw ssrbool.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5178,14 +5118,15 @@ The view mechanism is compatible with reflect predicates.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all abort
 
+     From Corelib Require Import ssrbool.
+
      Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b.
      apply/andP.
 
@@ -5296,14 +5237,15 @@ but they also allow complex transformation, involving negations.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+
      Check introN.
 
   .. rocqtop:: all
@@ -5329,16 +5271,17 @@ actually uses its propositional interpretation.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+
      Lemma test (a b : bool) (pab : b && a) : b.
-     have /andP [pa ->] : (a && b) by rewrite andbC.
+     have /andP [pa ->] : (a && b) by rw andbC.
 
 Interpreting goals
 ``````````````````
@@ -5392,14 +5335,15 @@ In this context, the identity view can be used when no view has to be applied:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+
      Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3.
      apply/idP/idP.
 
@@ -5408,14 +5352,15 @@ In this context, the identity view can be used when no view has to be applied:
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+
      Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3.
      apply/norP/idP.
 
@@ -5484,15 +5429,17 @@ pass a given hypothesis to a lemma.
 
   .. rocqtop:: reset none
 
-     From Corelib Require Import ssreflect ssrbool.
+     From Corelib Require Import ssreflect_rw.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
-     Section Test.
-     Variables P Q R : Prop.
 
   .. rocqtop:: all
 
+     From Corelib Require Import ssrbool.
+     Section Test.
+     Variables P Q R : Prop.
+
      Variable P2Q : P -> Q.
      Variable Q2R : Q -> R.
 
@@ -5517,8 +5464,8 @@ The following intro pattern ltac views are provided:
 
 One can call rewrite from an intro pattern, use with parsimony:
 
-+ ``/[1! rules]`` shortcut for ``rewrite rules``
-+ ``/[! rules]`` shortcut for ``rewrite !rules``
++ ``/[1! rules]`` shortcut for ``rw rules``
++ ``/[! rules]`` shortcut for ``rw !rules``
 
 
 Synopsis and Index
@@ -5654,7 +5601,7 @@ respectively.
 
    case analysis (see :ref:`the_defective_tactics_ssr`)
 
-.. tacv:: rewrite {+ @r_step }
+.. tacv:: rw {+ @r_step }
 
    rewrite (see :ref:`rewriting_ssr`)
 
@@ -5787,3 +5734,54 @@ Commands
   Proof`` command of Rocq proof mode.
 .. [#10] A simple proof context entry is a naked identifier (i.e., not between
   parentheses) designating a context entry that is not a section variable.
+
+.. _compatibility_issues_ssr:
+
+
+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`
+creates an environment that is mostly
+compatible with the rest of Rocq, up to a few discrepancies.
+
++ New keywords (``is``) might clash with variable, constant, tactic or
+  tactical names, or with quasi-keywords in tactic or
+  notation commands.
++ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those
+  available in current versions of Rocq; in particular, ``rewrite .. in
+  (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite`
+  will not work, and the |SSR| syntax and semantics for occurrence selection
+  and rule chaining are different. Use an explicit rewrite direction
+  (``rewrite <- …`` or ``rewrite -> …``) to access the Rocq rewrite tactic.
++ The generalization of ``if`` statements to non-Boolean conditions is turned off
+  by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the
+  ``sumXXX`` types (declared in ``ssrfun.v``) and the
+  :n:`if @term is @pattern then @term else @term` construct
+  (see :ref:`pattern_conditional_ssr`).  To use the
+  generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
+  ``Close Scope boolean_if_scope``.
++ The following flag can be unset to make |SSR| more compatible with
+  parts of Rocq.
+
+.. flag:: SsrRewrite
+
+   Controls whether the incompatible rewrite syntax is enabled (the default).
+   Disabling the :term:`flag` makes the syntax compatible with other parts of Rocq.
+   Note that this ``rewrite`` syntax, now superseded by ``rw``, is
+   only activated when explicitly requiring the backward compatibility
+   module ``From Corelib Require Import ssreflect.``.
diff --git a/lib/deprecation.ml b/lib/deprecation.ml
index 41ed5fd5cf78..ad1c81abc2b7 100644
--- a/lib/deprecation.ml
+++ b/lib/deprecation.ml
@@ -102,6 +102,6 @@ module Version = struct
   let v9_3 = get_generic_cat "9.3"
   (* When adding a new version here, please also add
      #[export] Set Warnings "-deprecated-since-X.Y".
-     in theories/Compat/RocqX{Y-1}.v *)
+     in theories/Corelib/Compat/RocqX{Y-1}.v *)
 
 end
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 46a68fa762e7..b3575c44833c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -500,10 +500,10 @@ let string_of_genarg_arg (ArgumentType arg) =
 (* When the [ssreflect.SsrSynax] module is imported, ssreflect
    operates in reduced compatibility mode. During printing, we try to
    account for this when this module is imported. *)
-let { Goptions.get = ssr_loaded } =
-  Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SSR";"Loaded"] ~value:false ()
+let { Goptions.get = ssr_rewrite_loaded } =
+  Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SSRRewriteLoaded"] ~value:false ()
 
-  let pr_orient b = if b then if ssr_loaded () then str "-> " else mt () else str "<- "
+  let pr_orient b = if b then if ssr_rewrite_loaded () then str "-> " else mt () else str "<- "
 
   let pr_multi = let open Equality in function
     | Precisely 1 -> mt ()
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0f7602d255bb..5dfe18498fb7 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -164,7 +164,7 @@ val ltop : entry_relative_level
 val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) ->
   'a Genprint.top_printer
 
-val ssr_loaded : unit -> bool
+val ssr_rewrite_loaded : unit -> bool
 
 module Internal : sig
   val pr_tacvalue_ref : (env -> Tacarg.tacvalue -> Pp.t) ref
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ff39394f29c8..d9394b101ccb 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -48,6 +48,7 @@ open Genintern
 
 val f_avoid_ids : Id.Set.t TacStore.field
 val f_debug : debug_info TacStore.field
+val extract_loc : interp_sign -> Loc.t option
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
   Ltac_pretype.constr_under_binders Id.Map.t
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index b8f390ca7e57..bfbad25e5cc8 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -251,7 +251,7 @@ let add_internal_name pt = internal_names := pt :: !internal_names
 let is_internal_name s = List.exists (fun p -> p s) !internal_names
 
 let mk_internal_id s =
-  let s' = Printf.sprintf "_%s_" s in
+  let s' = Printf.sprintf "‗%s‗" s in
   let s' = String.map (fun c -> if c = ' ' then '_' else c) s' in
   add_internal_name ((=) s'); Id.of_string s'
 
@@ -262,19 +262,22 @@ let skip_digits s =
   let n = String.length s in
   let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop
 
-let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d_" t i)
+let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d‗" t i)
+(* [is_dll s n] test if character at pos [n] of [s] is UTF8 double low line '‗'.
+   Assumes [n] <= [String.length n - 3]. *)
+let is_dll s n = s.[n] = '\226' && s.[n+1] = '\128' && s.[n+2] = '\151'
 let is_tagged t s =
-  let n = String.length s - 1 and m = String.length t in
-  m < n && s.[n] = '_' && same_prefix s t m && skip_digits s m = n
+  let n = String.length s and m = String.length t in
+  m < n - 3 && is_dll s (n - 3) && same_prefix s t m && skip_digits s m = n - 3
 
-let evar_tag = "_evar_"
+let evar_tag = "‗evar_"
 let _ = add_internal_name (is_tagged evar_tag)
 let mk_evar_name n = Name (mk_tagged_id evar_tag n)
 
 let ssr_anon_hyp = "Hyp"
 
-let wildcard_tag = "_the_"
-let wildcard_post = "_wildcard_"
+let wildcard_tag = "‗the_"
+let wildcard_post = "_wildcard‗"
 let has_wildcard_tag s =
   let n = String.length s in let m = String.length wildcard_tag in
   let m' = String.length wildcard_post in
@@ -283,19 +286,19 @@ let has_wildcard_tag s =
   skip_digits s m = n - m' - 2
 let _ = add_internal_name has_wildcard_tag
 
-let discharged_tag = "_discharged_"
+let discharged_tag = "‗discharged_"
 let mk_discharged_id id =
-  Id.of_string (Printf.sprintf "%s%s_" discharged_tag (Id.to_string id))
+  Id.of_string (Printf.sprintf "%s%s‗" discharged_tag (Id.to_string id))
 let has_discharged_tag s =
-  let m = String.length discharged_tag and n = String.length s - 1 in
-  m < n && s.[n] = '_' && same_prefix s discharged_tag m
+  let m = String.length discharged_tag and n = String.length s in
+  m < n - 3 && is_dll s (n - 3) && same_prefix s discharged_tag m
 let _ = add_internal_name has_discharged_tag
 let is_discharged_id id = has_discharged_tag (Id.to_string id)
 
 let max_suffix m (t, j0 as tj0) id  =
-  let s = Id.to_string id in let n = String.length s - 1 in
-  let dn = String.length t - 1 - n in let i0 = j0 - dn in
-  if not (i0 >= m && s.[n] = '_' && same_prefix s t m) then tj0 else
+  let s = Id.to_string id in let n = String.length s - 3 in
+  let dn = String.length t - 3 - n in let i0 = j0 - dn in
+  if not (i0 >= m && is_dll s n && same_prefix s t m) then tj0 else
   let rec loop i =
     if i < i0 && s.[i] = '0' then loop (i + 1) else
     if (if i < i0 then skip_digits s i = n else le_s_t i) then s, i else tj0
@@ -309,9 +312,9 @@ let max_suffix m (t, j0 as tj0) id  =
 let mk_anon_id t gl_ids =
   let gl_ids = List.map NamedDecl.get_id (EConstr.named_context_of_val gl_ids) in
   let m, si0, id0 =
-    let s = ref (Printf.sprintf  "_%s_" t) in
-    if is_internal_name !s then s := "_" ^ !s;
-    let n = String.length !s - 1 in
+    let s = ref (Printf.sprintf  "‗%s‗" t) in
+    if is_internal_name !s then s := "‗" ^ !s;
+    let n = String.length !s - 3 in
     let rec loop i j =
       let d = !s.[i] in if not (is_digit d) then i + 1, j else
       loop (i - 1) (if d = '0' then j else i) in
@@ -320,10 +323,12 @@ let mk_anon_id t gl_ids =
   let s, i = List.fold_left (max_suffix m) si0 gl_ids in
   let open Bytes in
   let s = of_string s in
-  let n = length s - 1 in
+  let n = length s - 3 in
+  let cat_dll s =
+    set s (n + 1) '\226'; set s (n + 2) '\128'; cat s (of_string "\151") in
   let rec loop i =
     if get s i = '9' then (set s i '0'; loop (i - 1)) else
-    if i < m then (set s n '0'; set s m '1'; cat s (of_string "_")) else
+    if i < m then (set s n '0'; set s m '1'; cat_dll s) else
     (set s i (Char.chr (Char.code (get s i) + 1)); s) in
   Id.of_string_soft (Bytes.to_string (loop (n - 1)))
 
@@ -551,7 +556,7 @@ let nb_evar_deps = function
     let s = Id.to_string id in
     if not (is_tagged evar_tag s) then 0 else
     let m = String.length evar_tag in
-    (try int_of_string (String.sub s m (String.length s - 1 - m)) with e when CErrors.noncritical e -> 0)
+    (try int_of_string (String.sub s m (String.length s - 3 - m)) with e when CErrors.noncritical e -> 0)
   | _ -> 0
 
 let type_id env sigma t = Id.of_string (Namegen.hdchar env sigma t)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index eb0de8cda3d8..309fd844cd7f 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -149,6 +149,9 @@ val mkSsrConst : Environ.env -> Evd.evar_map -> string -> Evd.evar_map * EConstr
 
 val is_discharged_id : Id.t -> bool
 val mk_discharged_id : Id.t -> Id.t
+(* [is_dll s n] test if character at pos [n] of [s] is UTF8 double low line '‗'.
+   Assumes [n] < [String.length n - 3]. *)
+val is_dll : string -> int -> bool
 val is_tagged : string -> string -> bool
 val has_discharged_tag : string -> bool
 val ssrqid : string -> Libnames.qualid
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 57ccbf298144..3ab565e3dd48 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -41,19 +41,6 @@ open Ssrequality
 open Ssripats
 open Libobject
 
-(** Ssreflect load check. *)
-
-(* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only *)
-(* turn on its incompatible features (the new rewrite syntax, and the   *)
-(* reserved identifiers) when the theory library (ssreflect.v) has      *)
-(* has actually been required, or is being defined. Because this check  *)
-(* needs to be done often (for each identifier lookup), we implement    *)
-(* some caching, repeating the test only when the environment changes.  *)
-(*   We check for protect_term because it is the first constant loaded; *)
-(* ssr_have would ultimately be a better choice.                        *)
-
-let is_ssr_loaded = Pptactic.ssr_loaded
-
 }
 
 DECLARE PLUGIN "rocq-runtime.plugins.ssreflect"
@@ -1583,7 +1570,7 @@ END
 {
 
 let sq_brace_tacnames =
-   ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
+   ["first"; "solve"; "do"; "rewrite"; "rw"; "have"; "suffices"; "wlog"]
    (* "by" is a keyword *)
 
 let test_ssrseqvar =
@@ -1626,31 +1613,20 @@ let ltac_expr = Pltac.ltac_expr
 
 (* Since Rocq now does repeated internal checks of its external lexical *)
 (* rules, we now need to carve ssreflect reserved identifiers out of   *)
-(* out of the user namespace. We use identifiers of the form _id_ for  *)
-(* this purpose, e.g., we "anonymize" an identifier id as _id_, adding *)
-(* an extra leading _ if this might clash with an internal identifier. *)
-(*    We check for ssreflect identifiers in the ident grammar rule;    *)
-(* when the ssreflect Module is present this is normally an error,     *)
-(* but we provide a compatibility flag to reduce this to a warning.    *)
+(* the user namespace. We use identifiers of the form ‗id‗ for         *)
+(* this purpose, e.g., we "anonymize" an identifier id as ‗id‗, adding *)
+(* an extra leading ‗ if this might clash with an internal identifier. *)
+(*    We check for ssreflect identifiers in the ident grammar rule.    *)
 
 {
 
-let { Goptions.get = ssr_reserved_ids } =
-  Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SsrIdents"] ~value:true ()
-
 let is_ssr_reserved s =
-  let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_'
+  let n = String.length s in n > 6 && is_dll s 0 && is_dll s (n - 3)
 
 let ssr_id_of_string loc s =
-  if is_ssr_reserved s && is_ssr_loaded () then begin
-    if ssr_reserved_ids() then
-      CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved."))
-    else if is_internal_name s then
-      Feedback.msg_warning (str ("Conflict between " ^ s ^ " and ssreflect internal names."))
-    else Feedback.msg_warning (str (
-     "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n"
-  ^ "Scripts with explicit references to anonymous variables are fragile."))
-    end; Id.of_string s
+  if is_ssr_reserved s then begin
+    CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved."))
+  end; Id.of_string s
 
 let ssr_null_entry = Procq.Entry.(of_parser "ssr_null" { parser_fun = fun _ _ -> Ok () })
 
@@ -1663,7 +1639,7 @@ END
 
 {
 
-let perm_tag = "_perm_Hyp_"
+let perm_tag = "‗perm_Hyp_"
 let _ = add_internal_name (is_tagged perm_tag)
 
 }
@@ -1740,7 +1716,6 @@ module Internal = struct
   let pr_intros = pr_intros
   let pr_view = pr_view
   let pr_mult = pr_mult
-  let is_ssr_loaded = is_ssr_loaded
   let pr_hpats = pr_hpats
   let pr_fwd = pr_fwd
   let pr_hint = pr_hint
@@ -1752,5 +1727,3 @@ module Internal = struct
 end
 
 }
-
-(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a1d177156e4a..04d1096784b5 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -188,8 +188,6 @@ module Internal : sig
 
   val pr_mult : ssrmult -> Pp.t
 
-  val is_ssr_loaded : unit -> bool
-
   val pr_hpats : ssrhpats -> Pp.t
 
   val pr_fwd : (Ssrast.ssrfwdkind * Ssrast.ssrbindfmt list) * Ssrast.ast_closure_term -> Pp.t
diff --git a/plugins/ssr/ssrtacs.mlg b/plugins/ssr/ssrtacs.mlg
index eb63b42f655b..64e86faad268 100644
--- a/plugins/ssr/ssrtacs.mlg
+++ b/plugins/ssr/ssrtacs.mlg
@@ -740,41 +740,15 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs
 ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs }
 END
 
-{
-
-let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true
-
-let () =
-  Goptions.(declare_bool_option
-    { optstage = Summary.Stage.Synterp;
-      optkey   = ["SsrRewrite"];
-      optread  = (fun _ -> !ssr_rw_syntax);
-      optdepr  = None;
-      optwrite = (fun b -> ssr_rw_syntax := b) })
-
-let lbrace = Char.chr 123
-(** Workaround to a limitation of coqpp *)
-
-let test_ssr_rw_syntax =
-  let test kwstate strm =
-    if not !ssr_rw_syntax then Error () else
-    if is_ssr_loaded () then Ok () else
-    match LStream.peek_nth kwstate 0 strm with
-    | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok ()
-    | _ -> Error () in
-  Procq.Entry.(of_parser "test_ssr_rw_syntax" { parser_fun = test })
-
-}
-
 GRAMMAR EXTEND Gram
   GLOBAL: ssrrwargs;
-  ssrrwargs: TOP [[ test_ssr_rw_syntax; a = LIST1 ssrrwarg -> { a } ]];
+  ssrrwargs: TOP [[ a = LIST1 ssrrwarg -> { a } ]];
 END
 
-(** The "rewrite" tactic *)
+(** The "rw" tactic *)
 
-TACTIC EXTEND ssrrewrite
-  | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] ->
+TACTIC EXTEND ssrrw
+  | [ "rw" ssrrwargs(args) ssrclauses(clauses) ] ->
     { tclCLAUSES (ssrrewritetac ist args) clauses }
 END
 
@@ -1050,5 +1024,3 @@ TACTIC EXTEND under
     Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
 END
-
-(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrtacs.mli b/plugins/ssr/ssrtacs.mli
index 4069c40ae277..062f2c1c2d43 100644
--- a/plugins/ssr/ssrtacs.mli
+++ b/plugins/ssr/ssrtacs.mli
@@ -10,6 +10,8 @@ open Ssrparser
 
 val wit_ssrarg : ssrarg Genarg.uniform_genarg_type
 val wit_ssrrwarg : ssrrwarg Genarg.uniform_genarg_type
+val ssrrwargs : ssrrwarg list Procq.Entry.t
+val pr_ssrrwargs : 'a -> 'b -> 'c -> ssrrwarg list -> Pp.t
 val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type
 
 val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d7995bd31af5..ccd46159c1d5 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -17,7 +17,6 @@ module CoqConstr = Constr
 open CoqConstr
 open Constrexpr
 open Constrexpr_ops
-open Procq
 open Procq.Prim
 open Procq.Constr
 open Pvernac.Vernac_
@@ -47,8 +46,6 @@ IGNORE KEYWORDS
 (** Alternative notations for "match" and anonymous arguments. *)(* ************)
 
 (* Syntax:                                                        *)
-(*  if <term> is <pattern> then ... else ...                      *)
-(*  if <term> is <pattern> [in ..] return ... then ... else ...   *)
 (*  let: <pattern> := <term> in ...                               *)
 (*  let: <pattern> [in ...] := <term> return ... in ...           *)
 (* The scope of a top-level 'as' in the pattern extends over the  *)
@@ -76,7 +73,6 @@ let aliasvar = function
 let mk_cnotype mp = aliasvar mp, None
 let mk_ctype mp t = aliasvar mp, Some t
 let mk_rtype t = Some t
-let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt
 let mk_let ?loc rt ct mp c1 =
   CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)])
 let mk_pat c (na, t) = (c, na, t)
@@ -87,25 +83,8 @@ GRAMMAR EXTEND Gram
   GLOBAL: term;
   ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
   ssr_mpat: [[ p = pattern -> { [[p]] } ]];
-  ssr_dpat: [
-    [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
-    | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt }
-    | mp = ssr_mpat -> { mp, no_ct, no_rt }
-  ] ];
-  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]];
-  ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
-  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
   term: LEVEL "10" [
-    [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
-      { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
-    | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
-      { let b1, ct, rt = db1 in
-      let b1, b2 = let open CAst in
-        let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
-        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
-      in
-      CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
-    | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
+    [ "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
       { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 }
     | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr;
       rt = ssr_rtype; "in"; c1 = lconstr ->
@@ -291,59 +270,3 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
        | Some k ->
           Ssrview.AdaptorDb.declare k hints }
 END
-
-(** Search compatibility *)
-
-{
-
-open G_vernac
-}
-
-GRAMMAR EXTEND Gram
-  GLOBAL: query_command;
-
-  query_command: TOP
-    [ [ IDENT "Search"; s = search_query; l = search_queries; "." ->
-          { let (sl,m) = l in
-            fun g ->
-              Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) }
-      ] ]
-;
-END
-
-(** Keyword compatibility fixes. *)
-
-(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
-(* identifiers used as keywords. This is incompatible with ssreflect.v *)
-(* which makes "by" and "of" true keywords, because of technicalities  *)
-(* in the internal lexer-parser API of Rocq. We patch this here by     *)
-(* adding new parsing rules that recognize the new keywords.           *)
-(*   To make matters worse, the Rocq grammar for tactics fails to      *)
-(* export the non-terminals we need to patch. Fortunately, the CamlP5  *)
-(* API provides a backdoor access (with loads of Obj.magic trickery).  *)
-
-(* Coq v8.3 defines "by" as a keyword, some hacks are not needed any   *)
-(* longer and thus comment out. Such comments are marked with v8.3     *)
-
-{
-
-open Pltac
-
-}
-
-GRAMMAR EXTEND Gram
-  GLOBAL: hypident;
-  hypident: TOP [
-  [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypTypeOnly }
-  | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypValueOnly }
-  ] ];
-END
-
-GRAMMAR EXTEND Gram
-  GLOBAL: constr_eval;
-  constr_eval: TOP [
-    [ IDENT "type"; "of"; c = Constr.constr -> { Tacexpr.ConstrTypeOf c }]
-  ];
-END
-
-(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssrrewrite/dune b/plugins/ssrrewrite/dune
new file mode 100644
index 000000000000..55f94c46ba44
--- /dev/null
+++ b/plugins/ssrrewrite/dune
@@ -0,0 +1,11 @@
+(library
+ (name ssreflect_rewrite_plugin)
+ (public_name rocq-runtime.plugins.ssreflect_rewrite)
+ (synopsis "Rocq's ssreflect plugin for rewrite compatibility")
+ (flags :standard -open Gramlib)
+ (libraries rocq-runtime.plugins.ssrmatching rocq-runtime.plugins.ssreflect))
+
+(rule
+ (targets ssrrewrite.ml)
+ (deps (:mlg ssrrewrite.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
diff --git a/plugins/ssrrewrite/ssrrewrite.mlg b/plugins/ssrrewrite/ssrrewrite.mlg
new file mode 100644
index 000000000000..cf1667041ffa
--- /dev/null
+++ b/plugins/ssrrewrite/ssrrewrite.mlg
@@ -0,0 +1,138 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+{
+
+open Constrexpr
+open Procq.Constr
+open Ltac_plugin
+open Ssreflect_plugin.Ssrtacticals
+open Ssreflect_plugin.Ssrequality
+open Ssreflect_plugin.Ssrparser
+open Ssreflect_plugin.Ssrtacs
+
+let warn_deprecated_rewrite =
+  CWarnings.create ~name:"rewrite-rw" ~category:Deprecation.Version.v9_3
+    ~quickfix:(fun ~loc () -> [Quickfix.make ~loc (Pp.str "rw")])
+    (fun () -> Pp.str "The 'rewrite' tactic has been renamed 'rw'.")
+
+}
+
+DECLARE PLUGIN "rocq-runtime.plugins.ssreflect_rewrite"
+
+(* The user is supposed to Require Import ssreflect or Require ssreflect   *)
+(* and Import ssreflect.SsrSyntax to obtain these keywords and as a        *)
+(* consequence the extended ssreflect grammar.                             *)
+IGNORE KEYWORDS
+
+(* type ssrrwargs = ssrrwarg list *)
+
+ARGUMENT EXTEND ssrrewriteargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs }
+END
+
+{
+
+let ssr_rewrite_syntax = Summary.ref ~name:"SSR:rewrite" true
+
+let () =
+  Goptions.(declare_bool_option
+    { optstage = Summary.Stage.Synterp;
+      optkey   = ["SsrRewrite"];
+      optread  = (fun _ -> !ssr_rewrite_syntax);
+      optdepr  = None;
+      optwrite = (fun b -> ssr_rewrite_syntax := b) })
+
+let lbrace = Char.chr 123
+(** Workaround to a limitation of coqpp *)
+
+let test_ssr_rewrite_syntax =
+  let test kwstate strm =
+    if not !ssr_rewrite_syntax then Error () else
+    if Pptactic.ssr_rewrite_loaded () then Ok () else
+    match LStream.peek_nth kwstate 0 strm with
+    | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok ()
+    | _ -> Error () in
+  Procq.Entry.(of_parser "test_ssr_rewrite_syntax" { parser_fun = test })
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: ssrrewriteargs;
+  ssrrewriteargs: TOP [[ test_ssr_rewrite_syntax; a = ssrrwargs -> { a } ]];
+END
+
+(** The "rewrite" tactic *)
+
+TACTIC EXTEND ssrrewrite
+  | [ "rewrite" ssrrewriteargs(args) ssrclauses(clauses) ] ->
+    { let loc = Tacinterp.extract_loc ist
+        |> Option.map (fun l -> Loc.sub l 0 7) in
+      warn_deprecated_rewrite ?loc ();
+      tclCLAUSES (ssrrewritetac ist args) clauses }
+END
+
+{
+
+(* global syntactic changes and vernacular commands *)
+
+(** Alternative notations for "match" and anonymous arguments. *)(* ************)
+
+(* Syntax:                                                        *)
+(*  if <term> is <pattern> then ... else ...                      *)
+(*  if <term> is <pattern> [in ..] return ... then ... else ...   *)
+(* The scope of a top-level 'as' in the pattern extends over the  *)
+(* 'return' type (dependent if/let).                              *)
+(* in b       (*^--ALTERNATIVE INNER LET--------^ *)              *)
+
+(* Caveat : There is no pretty-printing support, since this would *)
+(* require a modification to the Rocq kernel (adding a new match  *)
+(* display style -- why aren't these strings?); also, the v8.1    *)
+(* pretty-printer only allows extension hooks for printing        *)
+(* integer or string literals.                                    *)
+(*   Also note that in the v8 grammar "is" needs to be a keyword; *)
+(* as this can't be done from an ML extension file, the new       *)
+(* syntax will only work when ssreflect.v is imported.            *)
+
+let no_ct = None, None and no_rt = None
+let aliasvar = function
+  | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na
+  | _ -> None
+let mk_cnotype mp = aliasvar mp, None
+let mk_ctype mp t = aliasvar mp, Some t
+let mk_rtype t = Some t
+let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt
+let mk_pat c (na, t) = (c, na, t)
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: term;
+  ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
+  ssr_mpat: [[ p = pattern -> { [[p]] } ]];
+  ssr_dpat: [
+    [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
+    | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt }
+    | mp = ssr_mpat -> { mp, no_ct, no_rt }
+  ] ];
+  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]];
+  ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
+  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
+  term: LEVEL "10" [
+    [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
+      { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
+    | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
+      { let b1, ct, rt = db1 in
+      let b1, b2 = let open CAst in
+        let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
+        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
+      in
+      CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
+  ] ];
+END
diff --git a/plugins/ssrrewrite/ssrrewrite.mli b/plugins/ssrrewrite/ssrrewrite.mli
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/test-suite/bugs/bug_4966.v b/test-suite/bugs/bug_4966.v
index 16dc0d113efc..05e93431c59b 100644
--- a/test-suite/bugs/bug_4966.v
+++ b/test-suite/bugs/bug_4966.v
@@ -1,7 +1,7 @@
 (* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *)
 
 Axiom proof_admitted : False.
-#[export] Hint Extern 0 => case proof_admitted : unused.
+#[export] Hint Extern 0 => (case proof_admitted) : unused.
 Ltac do_tac tac := tac.
 
 Goal False.
diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v
index 5328f35d70fc..d100488d0abb 100644
--- a/test-suite/output/ssr_under.v
+++ b/test-suite/output/ssr_under.v
@@ -10,7 +10,7 @@ Axiom eq_G :
 Ltac show := match goal with [|-?g] => idtac g end.
 
 Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-under eq_G => m do [show; rewrite subnn].
+under eq_G => m do [show; rw subnn].
 show.
 Abort.
 
diff --git a/theories/Corelib/ssr/ssrbool.v b/theories/Corelib/ssr/ssrbool.v
index 514a9b427541..a1d23ba841a8 100644
--- a/theories/Corelib/ssr/ssrbool.v
+++ b/theories/Corelib/ssr/ssrbool.v
@@ -557,7 +557,7 @@ Lemma contraTnot (b : bool) (P : Prop) : (P -> ~~ b) -> (b -> ~ P).
 Proof. by case: b; auto. Qed.
 
 Lemma contraNnot (P : Prop) (b : bool) : (P -> b) -> (~~ b -> ~ P).
-Proof. rewrite -{1}[b]negbK; exact: contraTnot. Qed.
+Proof. rw -{1}[b]negbK; exact: contraTnot. Qed.
 
 Lemma contraPT (P : Prop) (b : bool) : (~~ b -> ~ P) -> P -> b.
 Proof. by case: b => //= /(_ isT) nP /nP. Qed.
@@ -566,7 +566,7 @@ Lemma contra_notT (P : Prop) (b : bool) : (~~ b -> P) -> ~ P -> b.
 Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed.
 
 Lemma contra_notN (P : Prop) (b : bool) : (b -> P) -> ~ P -> ~~ b.
-Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed.
+Proof. rw -{1}[b]negbK; exact: contra_notT. Qed.
 
 Lemma contraPN (P : Prop) (b : bool) : (b -> ~ P) -> (P -> ~~ b).
 Proof. by case: b => //=; move/(_ isT) => HP /HP. Qed.
@@ -620,7 +620,7 @@ Lemma ifP : if_spec (b = false) b (if b then vT else vF).
 Proof. by case def_b: b; constructor. Qed.
 
 Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).
-Proof. by case def_b: b; constructor; rewrite ?def_b. Qed.
+Proof. by case def_b: b; constructor; rw ?def_b. Qed.
 
 Lemma ifT : b -> (if b then vT else vF) = vT. Proof. by move->. Qed.
 Lemma ifF : b = false -> (if b then vT else vF) = vF. Proof. by move->. Qed.
@@ -686,10 +686,10 @@ Lemma elimTFn : b = c -> if c then ~ P else P.
 Proof. by move <-; apply: (elimNTF Hb); case b. Qed.
 
 Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
-Proof. by rewrite -if_neg; apply: equivPif. Qed.
+Proof. by rw -if_neg; apply: equivPif. Qed.
 
 Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
-Proof. by rewrite -if_neg; apply: xorPif. Qed.
+Proof. by rw -if_neg; apply: xorPif. Qed.
 
 End ReflectNegCore.
 
@@ -746,7 +746,7 @@ Variant alt_spec : bool -> Type :=
   | AltFalse of ~~ b : alt_spec false.
 
 Lemma altP : alt_spec b.
-Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed.
+Proof. by case def_b: b / Pb; constructor; rw ?def_b. Qed.
 
 Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2.
 Proof. by move->. Qed.
@@ -1159,13 +1159,13 @@ Arguments addbP {a b}.
 Ltac bool_congr :=
   match goal with
   | |- (?X1 && ?X2 = ?X3) => first
-  [ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
-  | case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ]
+  [ symmetry; rw -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
+  | case: (X1); [ rw ?andTb ?andbT // | by rw ?andbF /= ] ]
   | |- (?X1 || ?X2 = ?X3) => first
-  [ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
-  | case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ]
+  [ symmetry; rw -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
+  | case: (X1); [ by rw ?orbT //= | rw ?orFb ?orbF ] ]
   | |- (?X1 (+) ?X2 = ?X3) =>
-    symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
+    symmetry; rw -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
   | |- (~~ ?X1 = ?X2) => congr 1 negb
   end.
 
@@ -1580,7 +1580,7 @@ Lemma mem_topred pT (pp : pT) : mem (topred pp) = mem pp.
 Proof. by case: pT pp. Qed.
 
 Lemma topredE pT x (pp : pT) : topred pp x = (x \in pp).
-Proof. by rewrite -mem_topred. Qed.
+Proof. by rw -mem_topred. Qed.
 
 Lemma app_predE x p (ap : registered_applicative_pred p) : ap x = (x \in p).
 Proof. by case: ap => _ /= ->. Qed.
@@ -1776,10 +1776,10 @@ Section PER.
 Hypotheses (symR : symmetric) (trR : transitive).
 
 Lemma sym_left_transitive : left_transitive.
-Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed.
+Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rw // symR. Qed.
 
 Lemma sym_right_transitive : right_transitive.
-Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed.
+Proof. by move=> x y /sym_left_transitive Rxy z; rw !(symR z) Rxy. Qed.
 
 End PER.
 
@@ -1792,7 +1792,7 @@ Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z).
 Lemma equivalence_relP : equivalence_rel <-> reflexive /\ left_transitive.
 Proof.
 split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->].
-by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].
+by split=> [x | x y Rxy z]; [rw (eqiR x x x) | rw (eqiR x y z)].
 Qed.
 
 End RelationProperties.
@@ -1966,19 +1966,19 @@ Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}.
 Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed.
 
 Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
-Proof. by move=> fK D1y ->; rewrite fK. Qed.
+Proof. by move=> fK D1y ->; rw fK. Qed.
 
 Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
-Proof. by move=> fK D1x <-; rewrite fK. Qed.
+Proof. by move=> fK D1x <-; rw fK. Qed.
 
 Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}.
 Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed.
 
 Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
-Proof. by move=> fK D2fy ->; rewrite fK. Qed.
+Proof. by move=> fK D2fy ->; rw fK. Qed.
 
 Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
-Proof. by move=> fK D2fx <-; rewrite fK. Qed.
+Proof. by move=> fK D2fx <-; rw fK. Qed.
 
 Lemma inW_bij : bijective f -> {in D1, bijective f}.
 Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.
@@ -2007,21 +2007,21 @@ Qed.
 Lemma in_on1P : {in D1, {on D2, allQ1 f}} <->
                 {in [pred x in D1 | f x \in D2], allQ1 f}.
 Proof.
-split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP.
+split => allf x; have := allf x; rw inE => Q1f; first by case/andP.
 by move=> ? ?; apply: Q1f; apply/andP.
 Qed.
 
 Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <->
                 {in [pred x in D1 | f x \in D2], allQ1l f h}.
 Proof.
-split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP.
+split => allf x; have := allf x; rw inE => Q1f; first by case/andP.
 by move=> ? ?; apply: Q1f; apply/andP.
 Qed.
 
 Lemma in_on2P : {in D1 &, {on D2 &, allQ2 f}} <->
                 {in [pred x in D1 | f x \in D2] &, allQ2 f}.
 Proof.
-split => allf x y; have := allf x y; rewrite !inE => Q2f.
+split => allf x y; have := allf x y; rw !inE => Q2f.
   by move=> /andP[? ?] /andP[? ?]; apply: Q2f.
 by move=> ? ? ? ?; apply: Q2f; apply/andP.
 Qed.
@@ -2098,12 +2098,12 @@ Arguments in_on2S  {T1 T2} D2 {f Q2}.
 
 Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT -> rT] [g : rT -> aT] :
   {in A, cancel f g} -> {in A, pcancel f (fun y : rT => Some (g y))}.
-Proof. by move=> fK x Ax; rewrite fK. Qed.
+Proof. by move=> fK x Ax; rw fK. Qed.
 
 Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}]
   [f : aT -> rT] [g : rT -> option aT] :
   {in A, pcancel f g} -> {in A &, injective f}.
-Proof. by move=> fK x y Ax Ay /(congr1 g); rewrite !fK// => -[]. Qed.
+Proof. by move=> fK x y Ax Ay /(congr1 g); rw !fK// => -[]. Qed.
 
 Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) :
   {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} ->
@@ -2117,14 +2117,14 @@ Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
   {homo h : x / x \in D' >-> x \in D} ->
   {in D, cancel f f'} -> {in D', cancel h h'} ->
   {in D', cancel (f \o h) (h' \o f')}.
-Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed.
+Proof. by move=> hD fK hK c cD /=; rw fK ?hK ?hD. Qed.
 
 Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
   [f : B -> A] [h : C -> B] [f' : A -> option B] [h' : B -> option C] :
   {homo h : x / x \in D' >-> x \in D} ->
   {in D, pcancel f f'} -> {in D', pcancel h h'} ->
   {in D', pcancel (f \o h) (obind h' \o f')}.
-Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed.
+Proof. by move=> hD fK hK c cD /=; rw fK/= ?hK ?hD. Qed.
 
 Definition pred_oapp T (D : {pred T}) : pred (option T) :=
   [pred x | oapp (mem D) false x].
@@ -2135,9 +2135,9 @@ Lemma ocan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
   {in D, ocancel f f'} -> {in D', ocancel h h'} ->
   {in D', ocancel (obind f \o h) (h' \o f')}.
 Proof.
-move=> hD fK hK c cD /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=.
-have bD : b \in D by have := hD _ cD; rewrite hcE inE.
-by rewrite -[b in RHS]fK; case: (f b) => //=; have /hK := cD; rewrite hcE.
+move=> hD fK hK c cD /=; rw -[RHS]hK/=; case hcE : (h c) => [b|]//=.
+have bD : b \in D by have := hD _ cD; rw hcE inE.
+by rw -[b in RHS]fK; case: (f b) => //=; have /hK := cD; rw hcE.
 Qed.
 
 Section in_sig.
@@ -2187,7 +2187,7 @@ Lemma equivalence_relP_in T (R : rel T) (A : pred T) :
    <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}}.
 Proof.
 split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; apply: Rxx.
-by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].
+by split=> [x Ax|x y Ax Ay Rxy z Az]; [rw (eqiR x x) | rw (eqiR x y)].
 Qed.
 
 Section MonoHomoMorphismTheory.
@@ -2196,41 +2196,41 @@ Variables (aT rT sT : Type) (f : aT -> rT) (g : rT -> aT).
 Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
 
 Lemma monoW : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x}.
-Proof. by move=> hf x ax; rewrite hf. Qed.
+Proof. by move=> hf x ax; rw hf. Qed.
 
 Lemma mono2W :
   {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y}.
-Proof. by move=> hf x y axy; rewrite hf. Qed.
+Proof. by move=> hf x y axy; rw hf. Qed.
 
 Hypothesis fgK : cancel g f.
 
 Lemma homoRL :
   {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y).
-Proof. by move=> Hf x y /Hf; rewrite fgK. Qed.
+Proof. by move=> Hf x y /Hf; rw fgK. Qed.
 
 Lemma homoLR :
   {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y.
-Proof. by move=> Hf x y /Hf; rewrite fgK. Qed.
+Proof. by move=> Hf x y /Hf; rw fgK. Qed.
 
 Lemma homo_mono :
     {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} ->
   {mono g : x y / rR x y >-> aR x y}.
 Proof.
 move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|].
-by apply: contraNF=> /mf; rewrite !fgK.
+by apply: contraNF=> /mf; rw !fgK.
 Qed.
 
 Lemma monoLR :
   {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y).
-Proof. by move=> mf x y; rewrite -{1}[y]fgK mf. Qed.
+Proof. by move=> mf x y; rw -{1}[y]fgK mf. Qed.
 
 Lemma monoRL :
   {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y.
-Proof. by move=> mf x y; rewrite -{1}[x]fgK mf. Qed.
+Proof. by move=> mf x y; rw -{1}[x]fgK mf. Qed.
 
 Lemma can_mono :
   {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y}.
-Proof. by move=> mf x y /=; rewrite -mf !fgK. Qed.
+Proof. by move=> mf x y /=; rw -mf !fgK. Qed.
 
 End MonoHomoMorphismTheory.
 
@@ -2243,14 +2243,14 @@ Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
 Lemma mono1W_in :
     {in aD, {mono f : x / aP x >-> rP x}} ->
   {in aD, {homo f : x / aP x >-> rP x}}.
-Proof. by move=> hf x hx ax; rewrite hf. Qed.
+Proof. by move=> hf x hx ax; rw hf. Qed.
 #[deprecated(since="Coq 8.16", note="Use mono1W_in instead.")]
 Abbreviation mono2W_in := mono1W_in.
 
 Lemma monoW_in :
     {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
   {in aD &, {homo f : x y / aR x y >-> rR x y}}.
-Proof. by move=> hf x y hx hy axy; rewrite hf. Qed.
+Proof. by move=> hf x y hx hy axy; rw hf. Qed.
 
 Hypothesis fgK : {in rD, {on aD, cancel g & f}}.
 Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}.
@@ -2258,12 +2258,12 @@ Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}.
 Lemma homoRL_in :
     {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
   {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}.
-Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed.
+Proof. by move=> Hf x y hx hy /Hf; rw fgK ?mem_g// ?inE; apply. Qed.
 
 Lemma homoLR_in :
     {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
   {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}.
-Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed.
+Proof. by move=> Hf x y hx hy /Hf; rw fgK ?mem_g// ?inE; apply. Qed.
 
 Lemma homo_mono_in :
     {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
@@ -2271,23 +2271,23 @@ Lemma homo_mono_in :
   {in rD &, {mono g : x y / rR x y >-> aR x y}}.
 Proof.
 move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact.
-by apply: contraNF=> /mf; rewrite !fgK ?mem_g//; apply.
+by apply: contraNF=> /mf; rw !fgK ?mem_g//; apply.
 Qed.
 
 Lemma monoLR_in :
     {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
   {in aD & rD, forall x y, rR (f x) y = aR x (g y)}.
-Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK ?mem_g// mf ?mem_g. Qed.
+Proof. by move=> mf x y hx hy; rw -{1}[y]fgK ?mem_g// mf ?mem_g. Qed.
 
 Lemma monoRL_in :
     {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
   {in rD & aD, forall x y, rR x (f y) = aR (g x) y}.
-Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK ?mem_g// mf ?mem_g. Qed.
+Proof. by move=> mf x y hx hy; rw -{1}[x]fgK ?mem_g// mf ?mem_g. Qed.
 
 Lemma can_mono_in :
     {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
   {in rD &, {mono g : x y / rR x y >-> aR x y}}.
-Proof. by move=> mf x y hx hy; rewrite -mf ?mem_g// !fgK ?mem_g. Qed.
+Proof. by move=> mf x y hx hy; rw -mf ?mem_g// !fgK ?mem_g. Qed.
 
 End MonoHomoMorphismTheory_in.
 Arguments homoRL_in {aT rT f g aD rD aR rR}.
@@ -2373,15 +2373,15 @@ Variables (f : aT -> rT) (g : rT -> aT).
 Lemma inj_can_sym_in_on :
     {homo f : x / x \in aD >-> x \in rD} -> {in aD, {on rD, cancel f & g}} ->
   {in rD &, {on aD &, injective g}} -> {in rD, {on aD, cancel g & f}}.
-Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rewrite ?inE ?fK ?fD. Qed.
+Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rw ?inE ?fK ?fD. Qed.
 
 Lemma inj_can_sym_on : {in aD, cancel f g} ->
   {on aD &, injective g} -> {on aD, cancel g & f}.
-Proof. by move=> fK gI x gx_aD; apply: gI; rewrite ?inE ?fK. Qed.
+Proof. by move=> fK gI x gx_aD; apply: gI; rw ?inE ?fK. Qed.
 
 Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} ->
   {in rD &, injective g} ->  {in rD, cancel g f}.
-Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed.
+Proof. by move=> fgD fK gI x x_rD; apply: gI; rw ?fK ?fgD. Qed.
 
 End inj_can_sym_in_on.
 Arguments inj_can_sym_in_on {aT rT aD rD f g}.
diff --git a/theories/Corelib/ssr/ssreflect.v b/theories/Corelib/ssr/ssreflect.v
index 0b36894e488d..284e34b14631 100644
--- a/theories/Corelib/ssr/ssreflect.v
+++ b/theories/Corelib/ssr/ssreflect.v
@@ -8,103 +8,29 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+Require Export ssreflect_rw.
+Declare ML Module "rocq-runtime.plugins.ssreflect_rewrite".
 
-(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+Module SsrIsSyntax.
 
-Require Import ssrmatching.
-Declare ML Module "rocq-runtime.plugins.ssreflect".
+(** Declare Ssr keywords: "is" "isn't". **)
+Reserved Notation "(******* x 'is' y 'isn't' *******)".
 
-(**
- This file is the Gallina part of the ssreflect plugin implementation.
- Files that use the ssreflect plugin should always Require ssreflect and
- either Import ssreflect or Import ssreflect.SsrSyntax.
-   Part of the contents of this file is technical and will only interest
- advanced developers; in addition the following are defined:
-   #[#the str of v by f#]# == the Canonical s : str such that f s = v.
-        #[#the str of v#]# == the Canonical s : str that coerces to v.
-        argumentType c == the T such that c : forall x : T, P x.
-          returnType c == the R such that c : T -> R.
-     {type of c for s} == P s where c : forall x : T, P x.
-           nonPropType == an interface for non-Prop Types: a nonPropType coerces
-                          to a Type, and only types that do _not_ have sort
-                          Prop are canonical nonPropType instances. This is
-                          useful for applied views (see mid-file comment).
-             notProp T == the nonPropType instance for type T.
-           phantom T v == singleton type with inhabitant Phantom T v.
-               phant T == singleton type with inhabitant Phant v.
-                 =^~ r == the converse of rewriting rule r (e.g., in a
-                          rewrite multirule).
-             unkeyed t == t, but treated as an unkeyed matching pattern by
-                          the ssreflect matching algorithm.
-             nosimpl t == t, but on the right-hand side of Definition C :=
-                          nosimpl disables expansion of C by /=.
-              locked t == t, but locked t is not convertible to t.
-       locked_with k t == t, but not convertible to t or locked_with k' t
-                          unless k = k' (with k : unit). Rocq type-checking
-                          will be much more efficient if locked_with with a
-                          bespoke k is used for sealed definitions.
-          unlockable v == interface for sealed constant definitions of v.
-        Unlockable def == the unlockable that registers def : C = v.
-     #[#unlockable of C#]# == a clone for C of the canonical unlockable for the
-                          definition of C (e.g., if it uses locked_with).
-    #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be
-                          an explicit lambda expression.
-  -> The usage pattern for ADT operations is:
-       Definition foo_def x1 .. xn := big_foo_expression.
-       Fact foo_key : unit. Proof. by #[# #]#. Qed.
-       Definition foo := locked_with foo_key foo_def.
-       Canonical foo_unlockable := #[#unlockable fun foo#]#.
-     This minimizes the comparison overhead for foo, while still allowing
-     rewrite unlock to expose big_foo_expression.
-
-         #[#elaborate x#]# == triggers Rocq elaboration to fill the holes of the term x
-                          The main use case is to trigger typeclass inference in
-                          the body of a ssreflect have := #[#elaborate body#]#.
-
-  Additionally we provide default intro pattern ltac views:
-  - top of the stack actions:
-    => /#[#apply#]#     := => hyp {}/hyp
-    => /#[#swap#]#      := => x y; move: y x
-                      (also swap and preserves let bindings)
-    => /#[#dup#]#       := => x; have copy := x; move: copy x
-                      (also copies and preserves let bindings)
-  - calling rewrite from an intro pattern, use with parsimony:
-    => /#[#1! rules#]#  := rewrite rules
-    => /#[#! rules#]#   := rewrite !rules
-
- More information about these definitions and their use can be found in the
- ssreflect manual, and in specific comments below.                           **)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Module SsrSyntax.
-
-(** Declare Ssr keywords: "is" "isn't" "of" "//" "/=" and "//=". **)
-
-Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)".
+End SsrIsSyntax.
 
-(** Enable SSR features **)
-#[export] Set SSR Loaded.
+Export SsrIsSyntax.
 
-Reserved Notation "<hidden n >" (at level 0, n at level 0,
-  format "<hidden  n >").
-#[warning="-postfix-notation-not-level-1"]
-Reserved Notation "T (* n *)" (at level 200, format "T  (* n *)").
-
-End SsrSyntax.
-
-Export SsrMatchingSyntax.
-Export SsrSyntax.
+(** Signal that we have ssreflect version of rewrite (meaning
+ "rewrite a" must be printed "rewrite -> a" for compatibility). **)
+#[export] Set SSRRewriteLoaded.
 
 (** Save primitive notation that will be overloaded. **)
-Local Abbreviation RocqGenericIf c vT vF := (if c then vT else vF) (only parsing).
+Local Abbreviation RocqGenericIf c vT vF :=
+  (if c then vT else vF) (only parsing).
 Local Abbreviation RocqGenericDependentIf c x R vT vF :=
   (if c as x return R then vT else vF) (only parsing).
 
-(** Reserve notation that introduced in this file. **)
+(** Reserve notations that are introduced in this file. **)
 Reserved Notation "'if' c 'then' vT 'else' vF" (at level 10,
   c, vT, vF at level 200).
 Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 10,
@@ -112,28 +38,6 @@ Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 10,
 Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 10,
   c, R, vT, vF at level 200, x name).
 
-Reserved Notation "[ 'the' sT 'of' v 'by' f ]" (at level 0,
-  format "[ 'the'  sT  'of'  v  'by'  f ]").
-Reserved Notation "[ 'the' sT 'of' v ]" (at level 0,
-  format "[ 'the'  sT  'of'  v ]").
-Reserved Notation "{ 'type' 'of' c 'for' s }" (at level 0,
-  format "{ 'type'  'of'  c  'for'  s }").
-
-Reserved Notation "=^~ r" (at level 100, format "=^~  r").
-
-Reserved Notation "[ 'unlockable' 'of' C ]" (at level 0,
-  format "[ 'unlockable'  'of'  C ]").
-Reserved Notation "[ 'unlockable' 'fun' C ]" (at level 0,
-  format "[ 'unlockable'  'fun'  C ]").
-
-Reserved Notation "[ 'elaborate' x ]" (at level 0).
-
-(**
- To define notations for tactic in intro patterns.
- When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **)
-Declare Scope ssripat_scope.
-Delimit Scope ssripat_scope with ssripat.
-
 (**
  Make the general "if" into a notation, so that we can override it below.
  The notations are "only parsing" because the Rocq decompiler will not
@@ -168,523 +72,10 @@ Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" :=
 
 Open Scope boolean_if_scope.
 
-(**
- To allow a wider variety of notations without reserving a large number of
- of identifiers, the ssreflect library systematically uses "forms" to
- enclose complex mixfix syntax. A "form" is simply a mixfix expression
- enclosed in square brackets and introduced by a keyword:
-      #[#keyword ... #]#
- Because the keyword follows a bracket it does not need to be reserved.
- Non-ssreflect libraries that do not respect the form syntax (e.g., the Rocq
- Lists library) should be loaded before ssreflect so that their notations
- do not mask all ssreflect forms.                                            **)
-Declare Scope form_scope.
-Delimit Scope form_scope with FORM.
-Open Scope form_scope.
-
-(**  Constants for abstract: and #[#: name #]# intro pattern  **)
-Definition abstract_lock := unit.
-Definition abstract_key := tt.
-
-Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
-  let: tt := lock in statement.
-
-Declare Scope ssr_scope.
-Notation "<hidden n >" := (abstract _ n _) : ssr_scope.
-Notation "T (* n *)" := (abstract T n abstract_key) : ssr_scope.
-Open Scope ssr_scope.
-
-Register abstract_lock as plugins.ssreflect.abstract_lock.
-Register abstract_key as plugins.ssreflect.abstract_key.
-Register abstract as plugins.ssreflect.abstract.
-
-(**  Constants for tactic-views  **)
-Inductive external_view : Type := tactic_view of Type.
-
-(**
- Syntax for referring to canonical structures:
-      #[#the struct_type of proj_val by proj_fun#]#
- This form denotes the Canonical instance s of the Structure type
- struct_type whose proj_fun projection is proj_val, i.e., such that
-      proj_fun s = proj_val.
- Typically proj_fun will be A record field accessors of struct_type, but
- this need not be the case; it can be, for instance, a field of a record
- type to which struct_type coerces; proj_val will likewise be coerced to
- the return type of proj_fun. In all but the simplest cases, proj_fun
- should be eta-expanded to allow for the insertion of implicit arguments.
-   In the common case where proj_fun itself is a coercion, the "by" part
- can be omitted entirely; in this case it is inferred by casting s to the
- inferred type of proj_val. Obviously the latter can be fixed by using an
- explicit cast on proj_val, and it is highly recommended to do so when the
- return type intended for proj_fun is "Type", as the type inferred for
- proj_val may vary because of sort polymorphism (it could be Set or Prop).
-   Note when using the #[#the _ of _ #]# form to generate a substructure from a
- telescopes-style canonical hierarchy (implementing inheritance with
- coercions), one should always project or coerce the value to the BASE
- structure, because Rocq will only find a Canonical derived structure for
- the Canonical base structure -- not for a base structure that is specific
- to proj_value.                                                              **)
-
-Module TheCanonical.
-
-Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put.
-
-Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
-
-Definition get_by vT sT & sT -> vT := @get vT sT.
-
-End TheCanonical.
-
-Import TheCanonical. (* Note: no export. *)
-
-Local Arguments get_by _%_type_scope _%_type_scope _ _ _ _.
-
-Notation "[ 'the' sT 'of' v 'by' f ]" :=
-  (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _))
-  (only parsing) : form_scope.
-
-Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*) s s) _))
-  (only parsing) : form_scope.
-
-(**
- The following are "format only" versions of the above notations.
- We need to do this to prevent the formatter from being be thrown off by
- application collapsing, coercion insertion and beta reduction in the right
- hand side of the notations above.                                           **)
-
-Notation "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
-  (only printing) : form_scope.
-
-Notation "[ 'the' sT 'of' v ]" := (@get _ sT v _ _)
-  (only printing) : form_scope.
-
-(**
- We would like to recognize
-Notation " #[# 'the' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _)
-  (at level 0, format " #[# 'the'  sT   'of'  v  :  'Type' #]#") : form_scope.
- **)
-
-(**
- Helper notation for canonical structure inheritance support.
- This is a workaround for the poor interaction between delta reduction and
- canonical projections in Rocq's unification algorithm, by which transparent
- definitions hide canonical instances, i.e., in
-   Canonical a_type_struct := @Struct a_type ...
-   Definition my_type := a_type.
- my_type doesn't effectively inherit the struct structure from a_type. Our
- solution is to redeclare the instance as follows
-   Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#.
- The special notation #[#str of _ #]# must be defined for each Structure "str"
- with constructor "Str", typically as follows
-   Definition clone_str s :=
-      let: Str _ x y ... z := s return {type of Str for s} -> str in
-      fun k => k _ x y ... z.
-    Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T))
-      (at level 0, format " #[# 'str'  'of'  T  'for'  s #]#") : form_scope.
-    Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x))
-      (at level 0, format " #[# 'str'  'of'  T #]#") : form_scope.
- The notation for the match return predicate is defined below; the eta
- expansion in the second form serves both to distinguish it from the first
- and to avoid the delta reduction problem.
-   There are several variations on the notation and the definition of the
- the "clone" function, for telescopes, mixin classes, and join (multiple
- inheritance) classes. We describe a different idiom for clones in ssrfun;
- it uses phantom types (see below) and static unification; see fintype and
- ssralg for examples.                                                        **)
-
-Definition argumentType T P & forall x : T, P x := T.
-Definition dependentReturnType T P & forall x : T, P x := P.
-Definition returnType aT rT & aT -> rT := rT.
-
-Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) : type_scope.
-
-(**
- A generic "phantom" type (actually, a unit type with a phantom parameter).
- This type can be used for type definitions that require some Structure
- on one of their parameters, to allow Rocq to infer said structure so it
- does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation
- (the latter interacts poorly with other Notation).
-   The definition of a (co)inductive type with a parameter p : p_type, that
- needs to use the operations of a structure
-  Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...}
- should be given as
-  Inductive indt_type (p : p_str) := Indt ... .
-  Definition indt_of (p : p_str) & phantom p_type p := indt_type p.
-  Notation "{ 'indt' p }" := (indt_of (Phantom p)).
-  Definition indt p x y ... z : {indt p} := @Indt p x y ... z.
-  Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z).
- That is, the concrete type and its constructor should be shadowed by
- definitions that use a phantom argument to infer and display the true
- value of p (in practice, the "indt" constructor often performs additional
- functions, like "locking" the representation -- see below).
-   We also define a simpler version ("phant" / "Phant") of phantom for the
- common case where p_type is Type.                                           **)
-
-Variant phantom T (p : T) : Prop := Phantom.
-Arguments phantom : clear implicits.
-Arguments Phantom : clear implicits.
-Variant phant (p : Type) : Prop := Phant.
-
-(**  Internal tagging used by the implementation of the ssreflect elim.  **)
-
-Definition protect_term (A : Type) (x : A) : A := x.
-
-Register protect_term as plugins.ssreflect.protect_term.
-
-(**
- The ssreflect idiom for a non-keyed pattern:
-  - unkeyed t will match any subterm that unifies with t, regardless of
-    whether it displays the same head symbol as t.
-  - unkeyed t a b will match any application of a term f unifying with t,
-    to two arguments unifying with a and b, respectively, regardless of
-    apparent head symbols.
-  - unkeyed x where x is a variable will match any subterm with the same
-    type as x (when x would raise the 'indeterminate pattern' error).        **)
-
+(* This abbreviation is only parsing in Prelude *)
 Abbreviation unkeyed x := (let flex := x in flex).
 
-(**  Ssreflect converse rewrite rule rule idiom.  **)
-Definition ssr_converse R (r : R) := (Logic.I, r).
-Notation "=^~ r" := (ssr_converse r) : form_scope.
-
-(**
- Term tagging (user-level).
- The ssreflect library uses four strengths of term tagging to restrict
- convertibility during type checking:
-  nosimpl t simplifies to t EXCEPT in a definition; more precisely, given
-    Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by
-    the /= and //= switches unless it is in a forcing context (e.g., in
-    match foo t' with ... end, foo t' will be reduced if this allows the
-    match to be reduced). Note that nosimpl bar is simply notation for a
-    a term that beta-iota reduces to bar; hence rewrite /foo will replace
-    foo by bar, and rewrite -/foo will replace bar by foo.
-    CAVEAT: nosimpl should not be used inside a Section, because the end of
-    section "cooking" removes the iota redex.
-  locked t is provably equal to t, but is not convertible to t; 'locked'
-    provides support for selective rewriting, via the lock t : t = locked t
-    Lemma, and the ssreflect unlock tactic.
-  locked_with k t is equal but not convertible to t, much like locked t,
-    but supports explicit tagging with a value k : unit. This is used to
-    mitigate a flaw in the term comparison heuristic of the Rocq kernel,
-    which treats all terms of the form locked t as equal and compares their
-    arguments recursively, leading to an exponential blowup of comparison.
-    For this reason locked_with should be used rather than locked when
-    defining ADT operations. The unlock tactic does not support locked_with
-    but the unlock rewrite rule does, via the unlockable interface.
-  we also use Module Type ascription to create truly opaque constants,
-    because simple expansion of constants to reveal an unreducible term
-    doubles the time complexity of a negative comparison. Such opaque
-    constants can be expanded generically with the unlock rewrite rule.
-    See the definition of card and subset in fintype for examples of this.   **)
-
-Abbreviation nosimpl t := (let: tt := tt in t).
-
-Lemma master_key : unit. Proof. exact tt. Qed.
-Definition locked A := let: tt := master_key in fun x : A => x.
-
-Register master_key as plugins.ssreflect.master_key.
-Register locked as plugins.ssreflect.locked.
-
-Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
-
-(**  The basic closing tactic "done".  **)
-Ltac done :=
-  trivial; hnf; intros; solve
-   [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial]
-         | discriminate | contradiction | split]
-   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
-
-(**  Quicker done tactic not including split, syntax: /0/  **)
-Ltac ssrdone0 :=
-  trivial; hnf; intros; solve
-   [ do ![solve [trivial | apply: sym_equal; trivial]
-         | discriminate | contradiction ]
-   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
-
-(**  To unlock opaque constants.  **)
-#[universes(template)]
-Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
-Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
-
-Notation "[ 'unlockable' 'of' C ]" :=
-  (@Unlockable _ _ C (unlock _)) : form_scope.
-
-Notation "[ 'unlockable' 'fun' C ]" :=
-  (@Unlockable _ (fun _ => _) C (unlock _)) : form_scope.
-
-(**  Generic keyed constant locking.  **)
-
-(**  The argument order ensures that k is always compared before T.  **)
-Definition locked_with k := let: tt := k in fun T x => x : T.
-
-(**
- This can be used as a cheap alternative to cloning the unlockable instance
- below, but with caution as unkeyed matching can be expensive.               **)
-Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
-Proof. by case: k. Qed.
-
-(**  Intensionaly, this instance will not apply to locked u.  **)
-Canonical locked_with_unlockable T k x :=
-  @Unlockable T x (locked_with k x) (locked_withE k x).
-
-(**  More accurate variant of unlock, and safer alternative to locked_withE. **)
-Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
-Proof. exact: unlock. Qed.
-
-(**  Abbreviation to trigger Rocq elaboration to fill the holes **)
-Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing).
-
-(**  The internal lemmas for the have tactics.  **)
-
-Lemma ssr_have
-  (Plemma : Prop)  (Pgoal : Prop)
-  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
-Proof. exact: rest step. Qed.
-
-Register ssr_have as plugins.ssreflect.ssr_have.
-
-Polymorphic Lemma ssr_have_upoly@{s1 s2;u1 u2}
-  (Plemma : Type@{s1;u1})  (Pgoal : Type@{s2;u2})
-  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
-Proof. exact: rest step. Qed.
-
-Register ssr_have_upoly as plugins.ssreflect.ssr_have_upoly.
-
-(**  Internal N-ary congruence lemmas for the congr tactic.  **)
-
-Fixpoint nary_congruence_statement (n : nat)
-         : (forall B, (B -> B -> Prop) -> Prop) -> Prop :=
-  match n with
-  | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2)
-  | S n' =>
-    let k' A B e (f1 f2 : A -> B) :=
-      forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in
-    fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e))
-  end.
-
-Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) :
-  nary_congruence_statement n k.
-Proof.
-have: k _ _ := _; rewrite {1}/k.
-elim: n k  => [|n IHn] k k_P /= A; first exact: k_P.
-by apply: IHn => B e He; apply: k_P => f x1 x2 <-.
-Qed.
-
-Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
-Proof. by move->. Qed.
-Arguments ssr_congr_arrow : clear implicits.
-
-Register nary_congruence as plugins.ssreflect.nary_congruence.
-Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow.
-
-(**  View lemmas that don't use reflection.  **)
-
-Section ApplyIff.
-
-Variables P Q : Prop.
-Hypothesis eqPQ : P <-> Q.
-
-Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed.
-Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed.
-
-Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed.
-Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed.
-
-End ApplyIff.
-
-Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2.
-Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
-
-(**
- To focus non-ssreflect tactics on a subterm, eg vm_compute.
- Usage:
-   elim/abstract_context: (pattern) => G defG.
-   vm_compute; rewrite {}defG {G}.
- Note that vm_cast are not stored in the proof term
- for reductions occurring in the context, hence
-   set here := pattern; vm_compute in (value of here)
- blows up at Qed time.                                        **)
-Lemma abstract_context T (P : T -> Type) x :
-  (forall Q, Q = P -> Q x) -> P x.
-Proof. by move=> /(_ P); apply. Qed.
-
-(*****************************************************************************)
-(* Material for under/over (to rewrite under binders using "context lemmas") *)
-
-Require Export ssrunder.
-
-#[global]
-Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) =>
-  solve [ apply: Under_rel.over_rel_done ] : core.
-#[global]
-Hint Resolve Under_rel.over_rel_done : core.
-
-Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
-Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel.
-
-(** Closing rewrite rule *)
-Definition over := over_rel.
-
-(** Closing tactic *)
-Ltac over :=
-  by [ apply: Under_rel.under_rel_done
-     | rewrite over
-     ].
-
-(** Convenience rewrite rule to unprotect evars, e.g., to instantiate
-    them in another way than with reflexivity. *)
-Definition UnderE := Under_relE.
-
-(*****************************************************************************)
-
-(** An interface for non-Prop types; used to avoid improper instantiation
-    of polymorphic lemmas with on-demand implicits when they are used as views.
-    For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y.
-    Using move/Some_inj on a goal of the form Some n = Some 0 will fail:
-    SSReflect will interpret the view as @Some_inj ?T _top_assumption_
-    since this is the well-typed application of the view with the minimal
-    number of inserted evars (taking ?T := Some n = Some 0), and then will
-    later complain that it cannot erase _top_assumption_ after having
-    abstracted the viewed assumption. Making x and y maximal implicits
-    would avoid this and force the intended @Some_inj nat x y _top_assumption_
-    interpretation, but is undesirable as it makes it harder to use Some_inj
-    with the many SSReflect and MathComp lemmas that have an injectivity
-    premise. Specifying {T : nonPropType} solves this more elegantly, as then
-    (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop.
- **)
-
-Module NonPropType.
-
-(** Implementation notes:
- We rely on three interface Structures:
-  - test_of r, the middle structure, performs the actual check: it has two
-    canonical instances whose 'condition' projection are maybeProj (?P : Prop)
-    and tt, and which set r := true and r := false, respectively. Unifying
-    condition (?t : test_of ?r) with maybeProj T will thus set ?r to true if
-    T is in Prop as the test_Prop T instance will apply, and otherwise simplify
-    maybeProp T to tt and use the test_negative instance and set ?r to false.
-  - call_of c r sets up a call to test_of on condition c with expected result r.
-    It has a default instance for its 'callee' projection to Type, which
-    sets c := maybeProj T and r := false when unifying with a type T.
-  - type is a telescope on call_of c r, which checks that unifying test_of ?r1
-    with c indeed sets ?r1 := r; the type structure bundles the 'test' instance
-    and its 'result' value along with its call_of c r projection. The default
-    instance essentially provides eta-expansion for 'type'. This is only
-    essential for the first 'result' projection to bool; using the instance
-    for other projection merely avoids spurious delta expansions that would
-    spoil the notProp T notation.
- In detail, unifying T =~= ?S with ?S : nonPropType, i.e.,
-  (1)  T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S)
- first uses the default call instance with ?T := T to reduce (1) to
-  (2a) @condition (result ?S) (test ?S) =~= maybeProp T
-  (3)                         result ?S =~= false
-  (4)                          frame ?S =~= call T
- along with some trivial universe-related checks which are irrelevant here.
-   Then the unification tries to use the test_Prop instance to reduce (2a) to
-  (6a)                        result ?S =~= true
-  (7a)                               ?P =~= T with ?P : Prop
-  (8a)                          test ?S =~= test_Prop ?P
- Now the default 'check' instance with ?result := true resolves (6a) as
-  (9a)                               ?S := @check true ?test ?frame
- Then (7a) can be solved precisely if T has sort at most (hence exactly) Prop,
- and then (8a) is solved by the check instance, yielding ?test := test_Prop T,
- and completing the solution of (2a), and _committing_ to it. But now (3) is
- inconsistent with (9a), and this makes the entire problem (1) fails.
-   If on the other hand T does not have sort Prop then (7a) fails and the
- unification resorts to delta expanding (2a), which gives
-  (2b) @condition (result ?S) (test ?S) =~= tt
- which is then reduced, using the test_negative instance, to
-  (6b)                        result ?S =~= false
-  (8b)                          test ?S =~= test_negative
- Both are solved using the check default instance, as in the (2a) branch, giving
-  (9b)                               ?S := @check false test_negative ?frame
- Then (3) and (4) are similarly solved using check, giving the final assignment
-  (9)                                ?S := notProp T
- Observe that we _must_ perform the actual test unification on the arguments
- of the initial canonical instance, and not on the instance itself as we do
- in mathcomp/matrix and mathcomp/vector, because we want the unification to
- fail when T has sort Prop. If both the test_of _and_ the result check
- unifications were done as part of the structure telescope then the latter
- would be a sub-problem of the former, and thus failing the check would merely
- make the test_of unification backtrack and delta-expand and we would not get
- failure.
- **)
-
-Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
-Definition maybeProp (T : Type) := tt.
-Definition call T := Call (maybeProp T) false T.
-
-Structure test_of (result : bool) := Test {condition :> unit}.
-Definition test_Prop (P : Prop) := Test true (maybeProp P).
-Definition test_negative := Test false tt.
-
-Structure type :=
-  Check {result : bool; test : test_of result; frame : call_of test result}.
-Definition check result test frame := @Check result test frame.
-
-Module Exports.
-Canonical call.
-Canonical test_Prop.
-Canonical test_negative.
-Canonical check.
-Abbreviation nonPropType := type.
-Coercion callee : call_of >-> Sortclass.
-Coercion frame : type >-> call_of.
-Abbreviation notProp T := (@check false test_negative (call T)).
-End Exports.
-
-End NonPropType.
-Export NonPropType.Exports.
-
-Module Export ipat.
-
-Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
-  (at level 0, only parsing) : ssripat_scope.
-
-(* we try to preserve the naming by matching the names from the goal *)
-(* we do move to perform a hnf before trying to match                *)
-Notation "'[' 'swap' ']'" := (ltac:(move;
-  let x := lazymatch goal with
-    | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_"
-  end in intro x; move;
-  let y := lazymatch goal with
-    | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_"
-  end in intro y; revert x; revert y))
-  (at level 0, only parsing) : ssripat_scope.
-
-
-(* we try to preserve the naming by matching the names from the goal *)
-(* we do move to perform a hnf before trying to match                *)
-Notation "'[' 'dup' ']'" := (ltac:(move;
-  lazymatch goal with
-  | |- forall (x : _), _ =>
-    let x := fresh x in intro x;
-    let copy := fresh x in have copy := x; revert x; revert copy
-  | |- let x := _ in _ =>
-    let x := fresh x in intro x;
-    let copy := fresh x in pose copy := x;
-    do [unfold x in (value of copy)]; revert x; revert copy
-  | |- _ =>
-    let x := fresh "_top_" in move=> x;
-    let copy := fresh "_top" in have copy := x; revert x; revert copy
-  end))
-  (at level 0, only parsing) : ssripat_scope.
-
-Notation "'[' '1' '!' rules ']'"     := (ltac:(rewrite rules))
-  (at level 0, rules at level 200, only parsing) : ssripat_scope.
-Notation "'[' '!' rules ']'"         := (ltac:(rewrite !rules))
-  (at level 0, rules at level 200, only parsing) : ssripat_scope.
-
-End ipat.
-
-(* A class to trigger reduction by rewriting.                           *)
-(* Usage: rewrite [pattern]vm_compute.                                  *)
-(* Alternatively one may redefine a lemma as in algebra/rat.v :         *)
-(* Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x. *)
-(* Proof. exact. Qed.                                                   *)
-
-Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y.
-
-#[global]
-Hint Extern 0 (@vm_compute_eq _ _ _) =>
-       vm_compute; reflexivity : typeclass_instances.
+Abbreviation phant := ssreflect_rw.phant.
+Abbreviation Phant := ssreflect_rw.Phant.
+Abbreviation phantom := ssreflect_rw.phantom.
+Abbreviation Phantom := ssreflect_rw.Phantom.
diff --git a/theories/Corelib/ssr/ssreflect_rw.v b/theories/Corelib/ssr/ssreflect_rw.v
new file mode 100644
index 000000000000..810e127f30ce
--- /dev/null
+++ b/theories/Corelib/ssr/ssreflect_rw.v
@@ -0,0 +1,643 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
+Require Import ssrmatching.
+Declare ML Module "rocq-runtime.plugins.ssreflect".
+
+(**
+ This file is the Gallina part of the ssreflect plugin implementation.
+ Files that use the ssreflect plugin should always Require ssreflect and
+ either Import ssreflect or Import ssreflect.SsrSyntax.
+   Part of the contents of this file is technical and will only interest
+ advanced developers; in addition the following are defined:
+   #[#the str of v by f#]# == the Canonical s : str such that f s = v.
+        #[#the str of v#]# == the Canonical s : str that coerces to v.
+        argumentType c == the T such that c : forall x : T, P x.
+          returnType c == the R such that c : T -> R.
+     {type of c for s} == P s where c : forall x : T, P x.
+           nonPropType == an interface for non-Prop Types: a nonPropType coerces
+                          to a Type, and only types that do _not_ have sort
+                          Prop are canonical nonPropType instances. This is
+                          useful for applied views (see mid-file comment).
+             notProp T == the nonPropType instance for type T.
+           phantom T v == singleton type with inhabitant Phantom T v.
+               phant T == singleton type with inhabitant Phant v.
+                 =^~ r == the converse of rewriting rule r (e.g., in a
+                          rewrite multirule).
+             unkeyed t == t, but treated as an unkeyed matching pattern by
+                          the ssreflect matching algorithm.
+             nosimpl t == t, but on the right-hand side of Definition C :=
+                          nosimpl disables expansion of C by /=.
+              locked t == t, but locked t is not convertible to t.
+       locked_with k t == t, but not convertible to t or locked_with k' t
+                          unless k = k' (with k : unit). Rocq type-checking
+                          will be much more efficient if locked_with with a
+                          bespoke k is used for sealed definitions.
+          unlockable v == interface for sealed constant definitions of v.
+        Unlockable def == the unlockable that registers def : C = v.
+     #[#unlockable of C#]# == a clone for C of the canonical unlockable for the
+                          definition of C (e.g., if it uses locked_with).
+    #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be
+                          an explicit lambda expression.
+  -> The usage pattern for ADT operations is:
+       Definition foo_def x1 .. xn := big_foo_expression.
+       Fact foo_key : unit. Proof. by #[# #]#. Qed.
+       Definition foo := locked_with foo_key foo_def.
+       Canonical foo_unlockable := #[#unlockable fun foo#]#.
+     This minimizes the comparison overhead for foo, while still allowing
+     rw unlock to expose big_foo_expression.
+
+         #[#elaborate x#]# == triggers Rocq elaboration to fill the holes of the term x
+                          The main use case is to trigger typeclass inference in
+                          the body of a ssreflect have := #[#elaborate body#]#.
+
+  Additionally we provide default intro pattern ltac views:
+  - top of the stack actions:
+    => /#[#apply#]#     := => hyp {}/hyp
+    => /#[#swap#]#      := => x y; move: y x
+                      (also swap and preserves let bindings)
+    => /#[#dup#]#       := => x; have copy := x; move: copy x
+                      (also copies and preserves let bindings)
+  - calling rw from an intro pattern, use with parsimony:
+    => /#[#1! rules#]#  := rw rules
+    => /#[#! rules#]#   := rw !rules
+
+ More information about these definitions and their use can be found in the
+ ssreflect manual, and in specific comments below.                           **)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Module SsrSyntax.
+
+(** Declare Ssr keywords: "//" "/=" and "//=". **)
+Reserved Notation "(******* // /= //= *******)".
+
+Reserved Notation "<hidden n >" (at level 0, n at level 0, only printing,
+  format "<hidden  n >").
+#[warning="-postfix-notation-not-level-1"]
+Reserved Notation "T (* n *)"
+  (at level 200, only printing, format "T  (* n *)").
+
+End SsrSyntax.
+
+Export SsrMatchingSyntax.
+Export SsrSyntax.
+
+(** Reserve notations that are introduced in this file. **)
+Reserved Notation "[ 'the' sT 'of' v 'by' f ]" (at level 0,
+  format "[ 'the'  sT  'of'  v  'by'  f ]").
+
+Reserved Notation "[ 'the' sT 'of' v ]" (at level 0,
+  format "[ 'the'  sT  'of'  v ]").
+Reserved Notation "{ 'type' 'of' c 'for' s }" (at level 0,
+  format "{ 'type'  'of'  c  'for'  s }").
+
+Reserved Notation "[ 'unlockable' 'of' C ]" (at level 0,
+  format "[ 'unlockable'  'of'  C ]").
+
+Reserved Notation "=^~ r" (at level 100, format "=^~  r").
+
+Reserved Notation "[ 'unlockable' 'fun' C ]" (at level 0,
+  format "[ 'unlockable'  'fun'  C ]").
+
+Reserved Notation "[ 'elaborate' x ]" (at level 0).
+
+(**
+ To define notations for tactic in intro patterns.
+ When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **)
+Declare Scope ssripat_scope.
+Delimit Scope ssripat_scope with ssripat.
+
+(**
+ To allow a wider variety of notations without reserving a large number
+ of identifiers, the ssreflect library systematically uses "forms" to
+ enclose complex mixfix syntax. A "form" is simply a mixfix expression
+ enclosed in square brackets and introduced by a keyword:
+      #[#keyword ... #]#
+ Because the keyword follows a bracket it does not need to be reserved.
+ Non-ssreflect libraries that do not respect the form syntax (e.g., the Rocq
+ Lists library) should be loaded before ssreflect so that their notations
+ do not mask all ssreflect forms.                                            **)
+Declare Scope form_scope.
+Delimit Scope form_scope with FORM.
+Open Scope form_scope.
+
+(**  Constants for abstract: and #[#: name #]# intro pattern  **)
+Definition abstract_lock := unit.
+Definition abstract_key := tt.
+
+Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
+  let: tt := lock in statement.
+
+Declare Scope ssr_scope.
+Notation "<hidden n >" := (abstract _ n _) (only printing) : ssr_scope.
+Notation "T (* n *)" := (abstract T n abstract_key) (only printing) : ssr_scope.
+Open Scope ssr_scope.
+
+Register abstract_lock as plugins.ssreflect.abstract_lock.
+Register abstract_key as plugins.ssreflect.abstract_key.
+Register abstract as plugins.ssreflect.abstract.
+
+(**  Constants for tactic-views  **)
+Inductive external_view : Type := tactic_view of Type.
+
+(**
+ Syntax for referring to canonical structures:
+      #[#the struct_type of proj_val by proj_fun#]#
+ This form denotes the Canonical instance s of the Structure type
+ struct_type whose proj_fun projection is proj_val, i.e., such that
+      proj_fun s = proj_val.
+ Typically proj_fun will be A record field accessors of struct_type, but
+ this need not be the case; it can be, for instance, a field of a record
+ type to which struct_type coerces; proj_val will likewise be coerced to
+ the return type of proj_fun. In all but the simplest cases, proj_fun
+ should be eta-expanded to allow for the insertion of implicit arguments.
+   In the common case where proj_fun itself is a coercion, the "by" part
+ can be omitted entirely; in this case it is inferred by casting s to the
+ inferred type of proj_val. Obviously the latter can be fixed by using an
+ explicit cast on proj_val, and it is highly recommended to do so when the
+ return type intended for proj_fun is "Type", as the type inferred for
+ proj_val may vary because of sort polymorphism (it could be Set or Prop).
+   Note when using the #[#the _ of _ #]# form to generate a substructure from a
+ telescopes-style canonical hierarchy (implementing inheritance with
+ coercions), one should always project or coerce the value to the BASE
+ structure, because Rocq will only find a Canonical derived structure for
+ the Canonical base structure -- not for a base structure that is specific
+ to proj_value.                                                              **)
+
+Module TheCanonical.
+
+Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put.
+
+Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
+
+Definition get_by vT sT & sT -> vT := @get vT sT.
+
+End TheCanonical.
+
+Import TheCanonical. (* Note: no export. *)
+
+Local Arguments get_by _%_type_scope _%_type_scope _ _ _ _.
+
+Notation "[ 'the' sT 'of' v 'by' f ]" :=
+  (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _))
+  (only parsing) : form_scope.
+
+Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*) s s) _))
+  (only parsing) : form_scope.
+
+(**
+ The following are "format only" versions of the above notations.
+ We need to do this to prevent the formatter from being be thrown off by
+ application collapsing, coercion insertion and beta reduction in the right
+ hand side of the notations above.                                           **)
+
+Notation "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
+  (only printing) : form_scope.
+
+Notation "[ 'the' sT 'of' v ]" := (@get _ sT v _ _)
+  (only printing) : form_scope.
+
+(**
+ We would like to recognize
+Notation " #[# 'the' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _)
+  (at level 0, format " #[# 'the'  sT   'of'  v  :  'Type' #]#") : form_scope.
+ **)
+
+(**
+ Helper notation for canonical structure inheritance support.
+ This is a workaround for the poor interaction between delta reduction and
+ canonical projections in Rocq's unification algorithm, by which transparent
+ definitions hide canonical instances, i.e., in
+   Canonical a_type_struct := @Struct a_type ...
+   Definition my_type := a_type.
+ my_type doesn't effectively inherit the struct structure from a_type. Our
+ solution is to redeclare the instance as follows
+   Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#.
+ The special notation #[#str of _ #]# must be defined for each Structure "str"
+ with constructor "Str", typically as follows
+   Definition clone_str s :=
+      let: Str _ x y ... z := s return {type of Str for s} -> str in
+      fun k => k _ x y ... z.
+    Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T))
+      (at level 0, format " #[# 'str'  'of'  T  'for'  s #]#") : form_scope.
+    Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x))
+      (at level 0, format " #[# 'str'  'of'  T #]#") : form_scope.
+ The notation for the match return predicate is defined below; the eta
+ expansion in the second form serves both to distinguish it from the first
+ and to avoid the delta reduction problem.
+   There are several variations on the notation and the definition of the
+ the "clone" function, for telescopes, mixin classes, and join (multiple
+ inheritance) classes. We describe a different idiom for clones in ssrfun;
+ it uses phantom types (see below) and static unification; see fintype and
+ ssralg for examples.                                                        **)
+
+Definition argumentType T P & forall x : T, P x := T.
+Definition dependentReturnType T P & forall x : T, P x := P.
+Definition returnType aT rT & aT -> rT := rT.
+
+Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) : type_scope.
+
+(**
+ A generic "phantom" type (actually, a unit type with a phantom parameter).
+ This type can be used for type definitions that require some Structure
+ on one of their parameters, to allow Rocq to infer said structure so it
+ does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation
+ (the latter interacts poorly with other Notation).
+   The definition of a (co)inductive type with a parameter p : p_type, that
+ needs to use the operations of a structure
+  Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...}
+ should be given as
+  Inductive indt_type (p : p_str) := Indt ... .
+  Definition indt_of (p : p_str) & phantom p_type p := indt_type p.
+  Notation "{ 'indt' p }" := (indt_of (Phantom p)).
+  Definition indt p x y ... z : {indt p} := @Indt p x y ... z.
+  Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z).
+ That is, the concrete type and its constructor should be shadowed by
+ definitions that use a phantom argument to infer and display the true
+ value of p (in practice, the "indt" constructor often performs additional
+ functions, like "locking" the representation -- see below).
+   We also define a simpler version ("phant" / "Phant") of phantom for the
+ common case where p_type is Type.                                           **)
+
+Variant phantom T (p : T) : Prop := Phantom.
+Arguments phantom : clear implicits.
+Arguments Phantom : clear implicits.
+Variant phant (p : Type) : Prop := Phant.
+
+(**  Internal tagging used by the implementation of the ssreflect elim.  **)
+
+Definition protect_term (A : Type) (x : A) : A := x.
+
+Register protect_term as plugins.ssreflect.protect_term.
+
+(**
+ The ssreflect idiom for a non-keyed pattern:
+  - unkeyed t will match any subterm that unifies with t, regardless of
+    whether it displays the same head symbol as t.
+  - unkeyed t a b will match any application of a term f unifying with t,
+    to two arguments unifying with a and b, respectively, regardless of
+    apparent head symbols.
+  - unkeyed x where x is a variable will match any subterm with the same
+    type as x (when x would raise the 'indeterminate pattern' error).        **)
+
+Abbreviation unkeyed x := (let flex := x in flex) (only parsing).
+
+(**  Ssreflect converse rewrite rule rule idiom.  **)
+Definition ssr_converse R (r : R) := (Logic.I, r).
+Notation "=^~ r" := (ssr_converse r) : form_scope.
+
+(**
+ Term tagging (user-level).
+ The ssreflect library uses four strengths of term tagging to restrict
+ convertibility during type checking:
+  nosimpl t simplifies to t EXCEPT in a definition; more precisely, given
+    Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by
+    the /= and //= switches unless it is in a forcing context (e.g., in
+    match foo t' with ... end, foo t' will be reduced if this allows the
+    match to be reduced). Note that nosimpl bar is simply notation for a
+    a term that beta-iota reduces to bar; hence rw /foo will replace
+    foo by bar, and rw -/foo will replace bar by foo.
+    CAVEAT: nosimpl should not be used inside a Section, because the end of
+    section "cooking" removes the iota redex.
+  locked t is provably equal to t, but is not convertible to t; 'locked'
+    provides support for selective rewriting, via the lock t : t = locked t
+    Lemma, and the ssreflect unlock tactic.
+  locked_with k t is equal but not convertible to t, much like locked t,
+    but supports explicit tagging with a value k : unit. This is used to
+    mitigate a flaw in the term comparison heuristic of the Rocq kernel,
+    which treats all terms of the form locked t as equal and compares their
+    arguments recursively, leading to an exponential blowup of comparison.
+    For this reason locked_with should be used rather than locked when
+    defining ADT operations. The unlock tactic does not support locked_with
+    but the unlock rewrite rule does, via the unlockable interface.
+  we also use Module Type ascription to create truly opaque constants,
+    because simple expansion of constants to reveal an unreducible term
+    doubles the time complexity of a negative comparison. Such opaque
+    constants can be expanded generically with the unlock rewrite rule.
+    See the definition of card and subset in fintype for examples of this.   **)
+
+Abbreviation nosimpl t := (let: tt := tt in t).
+
+Lemma master_key : unit. Proof. exact tt. Qed.
+Definition locked A := let: tt := master_key in fun x : A => x.
+
+Register master_key as plugins.ssreflect.master_key.
+Register locked as plugins.ssreflect.locked.
+
+Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
+
+(**  The basic closing tactic "done".  **)
+Ltac done :=
+  trivial; hnf; intros; solve
+   [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial]
+         | discriminate | contradiction | split]
+   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
+
+(**  Quicker done tactic not including split, syntax: /0/  **)
+Ltac ssrdone0 :=
+  trivial; hnf; intros; solve
+   [ do ![solve [trivial | apply: sym_equal; trivial]
+         | discriminate | contradiction ]
+   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
+
+(**  To unlock opaque constants.  **)
+#[universes(template)]
+Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
+Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
+
+Notation "[ 'unlockable' 'of' C ]" :=
+  (@Unlockable _ _ C (unlock _)) : form_scope.
+
+Notation "[ 'unlockable' 'fun' C ]" :=
+  (@Unlockable _ (fun _ => _) C (unlock _)) : form_scope.
+
+(**  Generic keyed constant locking.  **)
+
+(**  The argument order ensures that k is always compared before T.  **)
+Definition locked_with k := let: tt := k in fun T x => x : T.
+
+(**
+ This can be used as a cheap alternative to cloning the unlockable instance
+ below, but with caution as unkeyed matching can be expensive.               **)
+Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
+Proof. by case: k. Qed.
+
+(**  Intensionaly, this instance will not apply to locked u.  **)
+Canonical locked_with_unlockable T k x :=
+  @Unlockable T x (locked_with k x) (locked_withE k x).
+
+(**  More accurate variant of unlock, and safer alternative to locked_withE. **)
+Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
+Proof. exact: unlock. Qed.
+
+(**  Abbreviation to trigger Rocq elaboration to fill the holes **)
+Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing).
+
+(**  The internal lemmas for the have tactics.  **)
+
+Lemma ssr_have
+  (Plemma : Prop)  (Pgoal : Prop)
+  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
+Proof. exact: rest step. Qed.
+
+Register ssr_have as plugins.ssreflect.ssr_have.
+
+Polymorphic Lemma ssr_have_upoly@{s1 s2;u1 u2}
+  (Plemma : Type@{s1;u1})  (Pgoal : Type@{s2;u2})
+  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
+Proof. exact: rest step. Qed.
+
+Register ssr_have_upoly as plugins.ssreflect.ssr_have_upoly.
+
+(**  Internal N-ary congruence lemmas for the congr tactic.  **)
+
+Fixpoint nary_congruence_statement (n : nat)
+         : (forall B, (B -> B -> Prop) -> Prop) -> Prop :=
+  match n with
+  | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2)
+  | S n' =>
+    let k' A B e (f1 f2 : A -> B) :=
+      forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in
+    fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e))
+  end.
+
+Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) :
+  nary_congruence_statement n k.
+Proof.
+have: k _ _ := _; rw {1}/k.
+elim: n k  => [|n IHn] k k_P /= A; first exact: k_P.
+by apply: IHn => B e He; apply: k_P => f x1 x2 <-.
+Qed.
+
+Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
+Proof. by move->. Qed.
+Arguments ssr_congr_arrow : clear implicits.
+
+Register nary_congruence as plugins.ssreflect.nary_congruence.
+Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow.
+
+(**  View lemmas that don't use reflection.  **)
+
+Section ApplyIff.
+
+Variables P Q : Prop.
+Hypothesis eqPQ : P <-> Q.
+
+Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed.
+Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed.
+
+Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed.
+Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed.
+
+End ApplyIff.
+
+Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2.
+Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
+
+(**
+ To focus non-ssreflect tactics on a subterm, eg vm_compute.
+ Usage:
+   elim/abstract_context: (pattern) => G defG.
+   vm_compute; rw {}defG {G}.
+ Note that vm_cast are not stored in the proof term
+ for reductions occurring in the context, hence
+   set here := pattern; vm_compute in (value of here)
+ blows up at Qed time.                                        **)
+Lemma abstract_context T (P : T -> Type) x :
+  (forall Q, Q = P -> Q x) -> P x.
+Proof. by move=> /(_ P); apply. Qed.
+
+(*****************************************************************************)
+(* Material for under/over (to rewrite under binders using "context lemmas") *)
+
+Require Export ssrunder.
+
+#[global]
+Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) =>
+  solve [ apply: Under_rel.over_rel_done ] : core.
+#[global]
+Hint Resolve Under_rel.over_rel_done : core.
+
+Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
+Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel.
+
+(** Closing rewrite rule *)
+Definition over := over_rel.
+
+(** Closing tactic *)
+Ltac over :=
+  by [ apply: Under_rel.under_rel_done
+     | rw over
+     ].
+
+(** Convenience rewrite rule to unprotect evars, e.g., to instantiate
+    them in another way than with reflexivity. *)
+Definition UnderE := Under_relE.
+
+(*****************************************************************************)
+
+(** An interface for non-Prop types; used to avoid improper instantiation
+    of polymorphic lemmas with on-demand implicits when they are used as views.
+    For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y.
+    Using move/Some_inj on a goal of the form Some n = Some 0 will fail:
+    SSReflect will interpret the view as @Some_inj ?T _top_assumption_
+    since this is the well-typed application of the view with the minimal
+    number of inserted evars (taking ?T := Some n = Some 0), and then will
+    later complain that it cannot erase _top_assumption_ after having
+    abstracted the viewed assumption. Making x and y maximal implicits
+    would avoid this and force the intended @Some_inj nat x y _top_assumption_
+    interpretation, but is undesirable as it makes it harder to use Some_inj
+    with the many SSReflect and MathComp lemmas that have an injectivity
+    premise. Specifying {T : nonPropType} solves this more elegantly, as then
+    (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop.
+ **)
+
+Module NonPropType.
+
+(** Implementation notes:
+ We rely on three interface Structures:
+  - test_of r, the middle structure, performs the actual check: it has two
+    canonical instances whose 'condition' projection are maybeProj (?P : Prop)
+    and tt, and which set r := true and r := false, respectively. Unifying
+    condition (?t : test_of ?r) with maybeProj T will thus set ?r to true if
+    T is in Prop as the test_Prop T instance will apply, and otherwise simplify
+    maybeProp T to tt and use the test_negative instance and set ?r to false.
+  - call_of c r sets up a call to test_of on condition c with expected result r.
+    It has a default instance for its 'callee' projection to Type, which
+    sets c := maybeProj T and r := false when unifying with a type T.
+  - type is a telescope on call_of c r, which checks that unifying test_of ?r1
+    with c indeed sets ?r1 := r; the type structure bundles the 'test' instance
+    and its 'result' value along with its call_of c r projection. The default
+    instance essentially provides eta-expansion for 'type'. This is only
+    essential for the first 'result' projection to bool; using the instance
+    for other projection merely avoids spurious delta expansions that would
+    spoil the notProp T notation.
+ In detail, unifying T =~= ?S with ?S : nonPropType, i.e.,
+  (1)  T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S)
+ first uses the default call instance with ?T := T to reduce (1) to
+  (2a) @condition (result ?S) (test ?S) =~= maybeProp T
+  (3)                         result ?S =~= false
+  (4)                          frame ?S =~= call T
+ along with some trivial universe-related checks which are irrelevant here.
+   Then the unification tries to use the test_Prop instance to reduce (2a) to
+  (6a)                        result ?S =~= true
+  (7a)                               ?P =~= T with ?P : Prop
+  (8a)                          test ?S =~= test_Prop ?P
+ Now the default 'check' instance with ?result := true resolves (6a) as
+  (9a)                               ?S := @check true ?test ?frame
+ Then (7a) can be solved precisely if T has sort at most (hence exactly) Prop,
+ and then (8a) is solved by the check instance, yielding ?test := test_Prop T,
+ and completing the solution of (2a), and _committing_ to it. But now (3) is
+ inconsistent with (9a), and this makes the entire problem (1) fails.
+   If on the other hand T does not have sort Prop then (7a) fails and the
+ unification resorts to delta expanding (2a), which gives
+  (2b) @condition (result ?S) (test ?S) =~= tt
+ which is then reduced, using the test_negative instance, to
+  (6b)                        result ?S =~= false
+  (8b)                          test ?S =~= test_negative
+ Both are solved using the check default instance, as in the (2a) branch, giving
+  (9b)                               ?S := @check false test_negative ?frame
+ Then (3) and (4) are similarly solved using check, giving the final assignment
+  (9)                                ?S := notProp T
+ Observe that we _must_ perform the actual test unification on the arguments
+ of the initial canonical instance, and not on the instance itself as we do
+ in mathcomp/matrix and mathcomp/vector, because we want the unification to
+ fail when T has sort Prop. If both the test_of _and_ the result check
+ unifications were done as part of the structure telescope then the latter
+ would be a sub-problem of the former, and thus failing the check would merely
+ make the test_of unification backtrack and delta-expand and we would not get
+ failure.
+ **)
+
+Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
+Definition maybeProp (T : Type) := tt.
+Definition call T := Call (maybeProp T) false T.
+
+Structure test_of (result : bool) := Test {condition :> unit}.
+Definition test_Prop (P : Prop) := Test true (maybeProp P).
+Definition test_negative := Test false tt.
+
+Structure type :=
+  Check {result : bool; test : test_of result; frame : call_of test result}.
+Definition check result test frame := @Check result test frame.
+
+Module Exports.
+Canonical call.
+Canonical test_Prop.
+Canonical test_negative.
+Canonical check.
+Abbreviation nonPropType := type.
+Coercion callee : call_of >-> Sortclass.
+Coercion frame : type >-> call_of.
+Abbreviation notProp T := (@check false test_negative (call T)).
+End Exports.
+
+End NonPropType.
+Export NonPropType.Exports.
+
+Module Export ipat.
+
+Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
+  (at level 0, only parsing) : ssripat_scope.
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match                *)
+Notation "'[' 'swap' ']'" := (ltac:(move;
+  let x := lazymatch goal with
+    | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_"
+  end in intro x; move;
+  let y := lazymatch goal with
+    | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_"
+  end in intro y; revert x; revert y))
+  (at level 0, only parsing) : ssripat_scope.
+
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match                *)
+Notation "'[' 'dup' ']'" := (ltac:(move;
+  lazymatch goal with
+  | |- forall (x : _), _ =>
+    let x := fresh x in intro x;
+    let copy := fresh x in have copy := x; revert x; revert copy
+  | |- let x := _ in _ =>
+    let x := fresh x in intro x;
+    let copy := fresh x in pose copy := x;
+    do [unfold x in (value of copy)]; revert x; revert copy
+  | |- _ =>
+    let x := fresh "_top_" in move=> x;
+    let copy := fresh "_top" in have copy := x; revert x; revert copy
+  end))
+  (at level 0, only parsing) : ssripat_scope.
+
+Notation "'[' '1' '!' rules ']'"     := (ltac:(rw rules))
+  (at level 0, rules at level 200, only parsing) : ssripat_scope.
+Notation "'[' '!' rules ']'"         := (ltac:(rw !rules))
+  (at level 0, rules at level 200, only parsing) : ssripat_scope.
+
+End ipat.
+
+(* A class to trigger reduction by rewriting.                           *)
+(* Usage: rw [pattern]vm_compute.                                       *)
+(* Alternatively one may redefine a lemma as in algebra/rat.v :         *)
+(* Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x. *)
+(* Proof. exact. Qed.                                                   *)
+
+Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y.
+
+#[global]
+Hint Extern 0 (@vm_compute_eq _ _ _) =>
+       vm_compute; reflexivity : typeclass_instances.
diff --git a/theories/Corelib/ssr/ssrfun.v b/theories/Corelib/ssr/ssrfun.v
index e5e5d1376680..fa714ce2f55c 100644
--- a/theories/Corelib/ssr/ssrfun.v
+++ b/theories/Corelib/ssr/ssrfun.v
@@ -445,7 +445,7 @@ Lemma frefl f : eqfun f f. Proof. by []. Qed.
 Lemma fsym f g : eqfun f g -> eqfun g f. Proof. by move=> eq_fg x. Qed.
 
 Lemma ftrans f g h : eqfun f g -> eqfun g h -> eqfun f h.
-Proof. by move=> eq_fg eq_gh x; rewrite eq_fg. Qed.
+Proof. by move=> eq_fg eq_gh x; rw eq_fg. Qed.
 
 Lemma rrefl r : eqrel r r. Proof. by []. Qed.
 
@@ -470,7 +470,7 @@ Definition catcomp g f := comp f g.
 Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
 
 Lemma eq_comp f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
-Proof. by move=> eq_ff' eq_gg' x; rewrite /comp eq_gg' eq_ff'. Qed.
+Proof. by move=> eq_ff' eq_gg' x; rw /comp eq_gg' eq_ff'. Qed.
 
 End Composition.
 
@@ -509,7 +509,7 @@ Proof. by []. Qed.
 Lemma omap_id (x : option rT) : omap id x = x. Proof. by case: x. Qed.
 
 Lemma eq_omap (h : aT -> rT) : f =1 h -> omap f =1 omap h.
-Proof. by move=> Ef [?|] //=; rewrite Ef. Qed.
+Proof. by move=> Ef [?|] //=; rw Ef. Qed.
 
 Lemma omapEapp : omap f = oapp (olift f) None.
 Proof. by []. Qed.
@@ -680,7 +680,7 @@ Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)).
 Proof. by move=> fK x; congr (Some _). Qed.
 
 Lemma pcan_inj g : pcancel g -> injective.
-Proof. by move=> fK x y /(congr1 g); rewrite !fK => [[]]. Qed.
+Proof. by move=> fK x y /(congr1 g); rw !fK => [[]]. Qed.
 
 Lemma can_inj g : cancel g -> injective.
 Proof. by move/can_pcan; apply: pcan_inj. Qed.
@@ -707,7 +707,7 @@ Proof. by move=> injf [?|] [?|] //= [/injf->]. Qed.
 
 Lemma omapK {aT rT : Type} (f : aT -> rT) (g : rT -> aT) :
   cancel f g -> cancel (omap f) (omap g).
-Proof. by move=> fK [?|] //=; rewrite fK. Qed.
+Proof. by move=> fK [?|] //=; rw fK. Qed.
 
 Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
 Proof. by case. Qed.
@@ -736,28 +736,28 @@ Lemma inj_compr : injective (f \o h) -> injective h.
 Proof. by move=> injfh x y /(congr1 f) /injfh. Qed.
 
 Lemma can_comp f' h' : cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').
-Proof. by move=> fK hK x; rewrite /= fK hK. Qed.
+Proof. by move=> fK hK x; rw /= fK hK. Qed.
 
 Lemma pcan_pcomp f' h' :
   pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').
-Proof. by move=> fK hK x; rewrite /pcomp fK /= hK. Qed.
+Proof. by move=> fK hK x; rw /pcomp fK /= hK. Qed.
 
 Lemma ocan_comp [fo : B -> option A] [ho : C -> option B]
     [f' : A -> B] [h' : B -> C] :
   ocancel fo f' -> ocancel ho h' -> ocancel (obind fo \o ho) (h' \o f').
 Proof.
-move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (ho c) => [b|]//=.
-by rewrite -[b in RHS]fK; case: (fo b) => //=; have := hK c; rewrite hcE.
+move=> fK hK c /=; rw -[RHS]hK/=; case hcE : (ho c) => [b|]//=.
+by rw -[b in RHS]fK; case: (fo b) => //=; have := hK c; rw hcE.
 Qed.
 
 Lemma eq_inj : injective f -> f =1 g -> injective g.
-Proof. by move=> injf eqfg x y; rewrite -2!eqfg; apply: injf. Qed.
+Proof. by move=> injf eqfg x y; rw -2!eqfg; apply: injf. Qed.
 
 Lemma eq_can f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
-Proof. by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
+Proof. by move=> fK eqfg eqfg' x; rw -eqfg -eqfg'. Qed.
 
 Lemma inj_can_eq f' : cancel f f' -> injective f' -> cancel g f' -> f =1 g.
-Proof. by move=> fK injf' gK x; apply: injf'; rewrite fK. Qed.
+Proof. by move=> fK injf' gK x; apply: injf'; rw fK. Qed.
 
 End InjectionsTheory.
 
@@ -775,7 +775,7 @@ Proof. by case: bijf => g fK _; apply: can_inj fK. Qed.
 Lemma bij_can_sym f' : cancel f' f <-> cancel f f'.
 Proof.
 split=> fK; first exact: inj_can_sym fK bij_inj.
-by case: bijf => h _ hK x; rewrite -[x]hK fK.
+by case: bijf => h _ hK x; rw -[x]hK fK.
 Qed.
 
 Lemma bij_can_eq f' f'' : cancel f f' -> cancel f f'' -> f' =1 f''.