18 files changed, 95 insertions, 81 deletions
diff --git a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst
new file mode 100644
index 0000000000..7fe69c39c1
--- /dev/null
+++ b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Undocumented and experimental forward class hint feature ``:>>``.
+  Use ``:>`` (see :n:`@of_type`) instead
+  (`#13106 <https://github.com/coq/coq/pull/13106>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst
new file mode 100644
index 0000000000..95a9093272
--- /dev/null
+++ b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Undetected collision between a lonely notation and a notation in
+  scope at printing time
+  (`#12946 <https://github.com/coq/coq/pull/12946>`_,
+  fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
new file mode 100644
index 0000000000..0ab9a58e6f
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Drop prefixes from grammar non-terminal names,
+  e.g. "constr:global" -> "global", "Prim.name" -> "name".
+  Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`.
+  (`#13096 <https://github.com/coq/coq/pull/13096>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 479fa674f5..cda8a1b679 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -387,8 +387,8 @@ The syntax for adding a new ring is
       interpretation via ``Cp_phi`` (the evaluation function of power
       coefficient) is the original term, or returns ``InitialRing.NotConstant``
       if not a constant coefficient (i.e. |L_tac| is the inverse function of
-      ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
-      and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
+      ``Cp_phi``). See files ``plugins/ring/ZArithRing.v``
+      and ``plugins/ring/RealField.v`` for examples. By default the tactic
       does not recognize power expressions as ring expressions.
 
    :n:`sign @one_term`
@@ -396,7 +396,7 @@ The syntax for adding a new ring is
       outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
       term :token:`term` is a proof that a given sign function indicates expressions
       that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See
-      ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
+      ``plugins/ring/InitialRing.v`` for examples of sign function.
 
    :n:`div @one_term`
       allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with
@@ -405,7 +405,7 @@ The syntax for adding a new ring is
       euclidean division function (:n:`@one_term` has to be a proof of
       ``Ring_theory.div_theory``). For example, this function is called when
       trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
-      ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
+      ``plugins/ring/InitialRing.v`` for examples of div function.
 
    :n:`closed [ {+ @qualid } ]`
       to be documented
@@ -538,7 +538,7 @@ Dealing with fields
    The tactic must be loaded by ``Require Import Field``. New field
    structures can be declared to the system with the ``Add Field`` command
    (see below). The field of real numbers is defined in module ``RealField``
-   (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
+   (in ``plugins/ring``). It is exported by module ``Rbase``, so
    that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
    real numbers. Rational numbers in canonical form are also declared as
    a field in the module ``Qcanon``.
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 11162ec96b..d533470f22 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -298,7 +298,7 @@ Summary of the commands
 .. cmd:: Class @inductive_definition {* with @inductive_definition }
 
    The :cmd:`Class` command is used to declare a typeclass with parameters
-   :token:`binders` and fields the declared record fields.
+   :n:`{* @binder }` and fields the declared record fields.
 
    Like any command declaring a record, this command supports the
    :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
@@ -337,7 +337,7 @@ Summary of the commands
    fields defined by :token:`field_def`, where each field must be a declared field of
    the class.
 
-   An arbitrary context of :token:`binders` can be put after the name of the
+   An arbitrary context of :n:`{* @binder }` can be put after the name of the
    instance and before the colon to declare a parameterized instance. An
    optional priority can be declared, 0 being the highest priority as for
    :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index ee8784fc02..a8a574c861 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,11 +183,8 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'binders',
     'collection',
-    'modpath',
     'tactic',
-    'destruction_arg',
     'bindings',
     'induction_clause',
     'conversion',
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 768c83150e..f1ed64e52a 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -274,7 +274,7 @@ following rules.
 .. inference:: Prod-Type
 
    \WTEG{T}{s}
-   s \in \{\SProp, \Type{i}\}
+   s \in \{\SProp, \Type(i)\}
    \WTE{\Gamma::(x:T)}{U}{\Type(i)}
    --------------------------------
    \WTEG{∀ x:T,~U}{\Type(i)}
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 765373619f..485dfd964d 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -677,7 +677,7 @@ fixpoint equation can be proved.
 
 .. index::
   single: Fix_F (term)
-  single: fix_eq (term)
+  single: Fix_eq (term)
   single: Fix_F_inv (term)
   single: Fix_F_eq (term)
 
@@ -696,7 +696,7 @@ fixpoint equation can be proved.
    forall (x:A) (r:Acc x),
      F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
   Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
-  Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
+  Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
   End FixPoint.
   End Well_founded.
 
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index fe10e345cd..41e1c30f0d 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -138,7 +138,7 @@ has type :n:`@type`.
       | {| Variable | Variables }
       assumpt ::= {+ @ident_decl } @of_type
       ident_decl ::= @ident {? @univ_decl }
-      of_type ::= {| : | :> | :>> } @type
+      of_type ::= {| : | :> } @type
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
    the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 727177b23a..48647deeff 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -133,7 +133,7 @@ follows:
    Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
    Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
 
-The complete set of such operators can be obtained looking at the :g:`PArray` module.
+The rest of these operators can be found in the :g:`PArray` module.
 
 These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
 :g:`Print Assumptions` command.
@@ -150,7 +150,16 @@ extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
 can be taken from the kernel of Coq (see ``kernel/parray.ml``).
 
-Primitive arrays expose a functional interface, but they are internally
-implemented using a persistent data structure :cite:`ConchonFilliatre07wml`.
-Update and access to an element in the most recent copy of an array are
-constant time operations.
+Coq's primitive arrays are persistent data structures. Semantically, a set operation
+``t.[i <- a]`` represents a new array that has the same values as ``t``, except
+at position ``i`` where its value is ``a``. The array ``t`` still exists, can
+still be used and its values were not modified. Operationally, the implementation
+of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not
+copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`.
+In short, the implementation keeps one version of ``t`` as an OCaml native array and
+other versions as lists of modifications to ``t``. Accesses to the native array
+version are constant time operations. However, accesses to versions where all the cells of
+the array are modified have O(n) access time, the same as a list. The version that is kept as the native array
+changes dynamically upon each get and set call: the current list of modifications
+is applied to the native array and the lists of modifications of the other versions
+are updated so that they still represent the same values.
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index ca69072cb9..f8375e93ce 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax.
 
 The syntax is also supported in internal binders. For instance, in the
 following kinds of expressions, the type of each declaration present
-in :token:`binders` can be bracketed to mark the declaration as
+in :n:`{* @binder }` can be bracketed to mark the declaration as
 implicit:
 * :n:`fun (@ident:forall {* @binder }, @type) => @term`,
 * :n:`forall (@ident:forall {* @binder }, @type), @type`,
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e276a0edcb..4b1f312105 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4726,7 +4726,7 @@ Automating
 
 .. seealso::
 
-   File plugins/setoid_ring/RealField.v for an example of instantiation,
+   File plugins/ring/RealField.v for an example of instantiation,
    theory theories/Reals for many examples of use of field.
 
 Non-logical tactics
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e05be7c2c2..8e23e61018 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -203,7 +203,7 @@ Generation of inversion principles with ``Derive`` ``Inversion``
    This command generates an inversion principle for the
    :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
    of the generated principle.  The second :token:`ident` should be an inductive
-   predicate, and :token:`binders` the variables occurring in the term
+   predicate, and :n:`{* @binder }` the variables occurring in the term
    :token:`term`. This command generates the inversion lemma for the sort
    :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`.
    When applied, it is equivalent to having inverted the instance with the
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6ba53b581b..5148fa84c9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -429,10 +429,6 @@ Displaying information about notations
    productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
    and `tactic_then_gen` which are not shown and can't be printed.
 
-   The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify
-   what part of the grammar a nonterminal is from.  If you examine nonterminal definitions
-   in the source code, they are identified only by the name following the colon.
-
    Most of the grammar in the documentation was updated in 8.12 to make it accurate and
    readable.  This was done using a new developer tool that extracts the grammar from the
    source code, edits it and inserts it into the documentation files.  While the
@@ -467,11 +463,11 @@ Displaying information about notations
    `tactic_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
    which applies to the productions within it, such as the `try` construct::
 
-     Entry tactic:tactic_expr is
+     Entry tactic_expr is
      [ "5" RIGHTA
-       [ tactic:binder_tactic ]
+       [ binder_tactic ]
      | "4" LEFTA
-       [ SELF; ";"; tactic:binder_tactic
+       [ SELF; ";"; binder_tactic
        | SELF; ";"; SELF
        | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
      | "3" RIGHTA
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a22f7ae9f3..a9f9c805d8 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -615,7 +615,7 @@ of_type_with_opt_coercion: [
 ]
 
 of_type_with_opt_coercion: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
 ]
 
 attribute_value: [
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index ba07e6df0d..2a7b283f55 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -24,7 +24,7 @@
    (glob_files %{project_root}/plugins/nsatz/*.mlg)
    (glob_files %{project_root}/plugins/omega/*.mlg)
    (glob_files %{project_root}/plugins/rtauto/*.mlg)
-   (glob_files %{project_root}/plugins/setoid_ring/*.mlg)
+   (glob_files %{project_root}/plugins/ring/*.mlg)
    (glob_files %{project_root}/plugins/syntax/*.mlg)
    (glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
    ; Sphinx files
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..067050b4f5 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -685,10 +685,10 @@ command: [
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
-| "Add" "Ring" ident ":" constr OPT ring_mods      (* setoid_ring plugin *)
-| "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" constr OPT field_mods      (* setoid_ring plugin *)
-| "Print" "Fields"      (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" constr OPT ring_mods      (* ring plugin *)
+| "Print" "Rings"      (* ring plugin *)
+| "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
+| "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" reference reference reference ":" ident numnotoption
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
@@ -986,10 +986,7 @@ constructor: [
 ]
 
 of_type_with_opt_coercion: [
-| ":>>"
-| ":>" ">"
 | ":>"
-| ":" ">" ">"
 | ":" ">"
 | ":"
 ]
@@ -1744,10 +1741,10 @@ simple_tactic: [
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "rtauto"
-| "protect_fv" string "in" ident      (* setoid_ring plugin *)
-| "protect_fv" string      (* setoid_ring plugin *)
-| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
-| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
+| "protect_fv" string "in" ident      (* ring plugin *)
+| "protect_fv" string      (* ring plugin *)
+| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
+| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
 ]
 
 mlname: [
@@ -1761,7 +1758,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)
@@ -2532,31 +2528,31 @@ induction_clause_list: [
 ]
 
 ring_mod: [
-| "decidable" constr      (* setoid_ring plugin *)
-| "abstract"      (* setoid_ring plugin *)
-| "morphism" constr      (* setoid_ring plugin *)
-| "constants" "[" tactic "]"      (* setoid_ring plugin *)
-| "closed" "[" LIST1 global "]"      (* setoid_ring plugin *)
-| "preprocess" "[" tactic "]"      (* setoid_ring plugin *)
-| "postprocess" "[" tactic "]"      (* setoid_ring plugin *)
-| "setoid" constr constr      (* setoid_ring plugin *)
-| "sign" constr      (* setoid_ring plugin *)
-| "power" constr "[" LIST1 global "]"      (* setoid_ring plugin *)
-| "power_tac" constr "[" tactic "]"      (* setoid_ring plugin *)
-| "div" constr      (* setoid_ring plugin *)
+| "decidable" constr      (* ring plugin *)
+| "abstract"      (* ring plugin *)
+| "morphism" constr      (* ring plugin *)
+| "constants" "[" tactic "]"      (* ring plugin *)
+| "closed" "[" LIST1 global "]"      (* ring plugin *)
+| "preprocess" "[" tactic "]"      (* ring plugin *)
+| "postprocess" "[" tactic "]"      (* ring plugin *)
+| "setoid" constr constr      (* ring plugin *)
+| "sign" constr      (* ring plugin *)
+| "power" constr "[" LIST1 global "]"      (* ring plugin *)
+| "power_tac" constr "[" tactic "]"      (* ring plugin *)
+| "div" constr      (* ring plugin *)
 ]
 
 ring_mods: [
-| "(" LIST1 ring_mod SEP "," ")"      (* setoid_ring plugin *)
+| "(" LIST1 ring_mod SEP "," ")"      (* ring plugin *)
 ]
 
 field_mod: [
-| ring_mod      (* setoid_ring plugin *)
-| "completeness" constr      (* setoid_ring plugin *)
+| ring_mod      (* ring plugin *)
+| "completeness" constr      (* ring plugin *)
 ]
 
 field_mods: [
-| "(" LIST1 field_mod SEP "," ")"      (* setoid_ring plugin *)
+| "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
 numnotoption: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..cbef29fb39 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -114,7 +114,7 @@ ident_decl: [
 ]
 
 of_type: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
 ]
 
 qualid: [
@@ -892,10 +892,10 @@ command: [
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
-| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
-| "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
-| "Print" "Fields"      (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* ring plugin *)
+| "Print" "Rings"      (* ring plugin *)
+| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
+| "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
@@ -1268,7 +1268,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)
@@ -1280,23 +1279,23 @@ fun_scheme_arg: [
 ]
 
 ring_mod: [
-| "decidable" one_term      (* setoid_ring plugin *)
-| "abstract"      (* setoid_ring plugin *)
-| "morphism" one_term      (* setoid_ring plugin *)
-| "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "setoid" one_term one_term      (* setoid_ring plugin *)
-| "sign" one_term      (* setoid_ring plugin *)
-| "power" one_term "[" LIST1 qualid "]"      (* setoid_ring plugin *)
-| "power_tac" one_term "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "div" one_term      (* setoid_ring plugin *)
-| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
+| "decidable" one_term      (* ring plugin *)
+| "abstract"      (* ring plugin *)
+| "morphism" one_term      (* ring plugin *)
+| "constants" "[" ltac_expr "]"      (* ring plugin *)
+| "preprocess" "[" ltac_expr "]"      (* ring plugin *)
+| "postprocess" "[" ltac_expr "]"      (* ring plugin *)
+| "setoid" one_term one_term      (* ring plugin *)
+| "sign" one_term      (* ring plugin *)
+| "power" one_term "[" LIST1 qualid "]"      (* ring plugin *)
+| "power_tac" one_term "[" ltac_expr "]"      (* ring plugin *)
+| "div" one_term      (* ring plugin *)
+| "closed" "[" LIST1 qualid "]"      (* ring plugin *)
 ]
 
 field_mod: [
-| ring_mod      (* setoid_ring plugin *)
-| "completeness" one_term      (* setoid_ring plugin *)
+| ring_mod      (* ring plugin *)
+| "completeness" one_term      (* ring plugin *)
 ]
 
 numeral_modifier: [
@@ -1642,8 +1641,8 @@ simple_tactic: [
 | "nsatz_compute" one_term      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "protect_fv" string OPT ( "in" ident )
-| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
-| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
+| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
+| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
 | match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
 | match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
 | "classical_left"