Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax)

Reviewed-by: Zimmi48

11 files changed, 113 insertions, 97 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 4d9e8d8b3a..847abb33fc 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,12 +170,12 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
+.. cmd::  Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
 
    This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
    :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
 
-   The :token:`ident` gives a unique name to the morphism and it is used
+   The final :token:`ident` gives a unique name to the morphism and it is used
    by the command to generate fresh names for automatically provided
    lemmas used internally.
 
@@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident
+.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
 
-   This command declares ``f`` as a parametric morphism of signature ``sig``. The
-   identifier :token:`ident` gives a unique name to the morphism and it is used as
-   the base name of the typeclass instance definition and as the name of
-   the lemma that proves the well-definedness of the morphism. The
-   parameters of the morphism as well as the signature may refer to the
-   context of variables. The command asks the user to prove interactively
-   that ``f`` respects the relations identified from the signature.
+   This command declares a parametric morphism :n:`@ident {+ @term__1}` of
+   signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
+   name to the morphism and it is used as the base name of the typeclass
+   instance definition and as the name of the lemma that proves the
+   well-definedness of the morphism. The parameters of the morphism as well as
+   the signature may refer to the context of variables. The command asks the
+   user to prove interactively that the function denoted by the first
+   :token:`ident` respects the relations identified from the signature.
 
 .. example::
 
@@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
 
-.. cmd:: Add Morphism f : @ident
+.. cmd:: Add Morphism @ident : @ident
    :name: Add Morphism
 
    This command is restricted to the declaration of morphisms
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 9219aa21ca..ee417f269d 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -311,24 +311,24 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @class t1 … tn {? | priority } := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
-   :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
-   fields ``b1`` to ``bi``, where each field must be a declared field of
+   :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
+   fields defined by :token:`field_def`, where each field must be a declared field of
    the class.  Missing fields must be filled in interactive proof mode.
 
    An arbitrary context of :token:`binders` 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 is not specified, it defaults to the number
+   :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n {? | priority } := @term
+   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term
 
       This syntax is used for declaration of singleton class instances or
-      for directly giving an explicit term of type :n:`forall @binders, @class
-      @term__1 … @term__n`.  One need not even mention the unique field name for
+      for directly giving an explicit term of type :n:`forall @binders, @term__0
+      {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
    .. cmdv:: Global Instance
@@ -356,11 +356,11 @@ Summary of the commands
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to typeclasses.
 
-.. cmd:: Existing Instance {+ @ident} {? | priority }
+.. cmd:: Existing Instance {+ @ident} {? | @num}
 
    This command adds an arbitrary list of constants whose type ends with
    an applied typeclass to the instance database with an optional
-   priority.  It can be used for redeclaring instances at the end of
+   priority :token:`num`.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
@@ -408,7 +408,7 @@ few other commands related to typeclasses.
    + When considering local hypotheses, we use the union of all the modes
      declared in the given databases.
 
-   .. cmdv:: typeclasses eauto @num
+   .. tacv:: typeclasses eauto @num
 
       .. warning::
          The semantics for the limit :n:`@num`
@@ -417,7 +417,7 @@ few other commands related to typeclasses.
          counted, which might result in larger limits being necessary when
          searching with ``typeclasses eauto`` than with :tacn:`auto`.
 
-   .. cmdv:: typeclasses eauto with {+ @ident}
+   .. tacv:: typeclasses eauto with {+ @ident}
 
       This variant runs resolution with the given hint databases. It treats
       typeclass subgoals the same as other subgoals (no shelving of
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ccd25ec9f3..5e214f6f7f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor
 
   .. productionlist::
     record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `record_term`
+    field_def : `ident` [`binders`] := `term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions.
 
       Links :token:`type` to each :token:`ident`.
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
       Declare one or more variables with various types.
 
-   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
-             Hypothesis {+ ( {+ @ident } : @type) }
-             Hypotheses {+ ( {+ @ident } : @type) }
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
       :name: Variables; Hypothesis; Hypotheses
 
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
 .. cmd:: Let @ident := @term
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 5a1af9f9fa..8acbcbec8f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -616,34 +616,34 @@ has type :token:`type`.
 
       Adds several parameters with specification :token:`type`.
 
-   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
 
       Adds blocks of parameters with different specifications.
 
-   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
       :name: Local Parameter
 
       Such parameters are never made accessible through their unqualified name by
       :cmd:`Import` and its variants. You have to explicitly give their fully
       qualified name to refer to them.
 
-   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
-             {? Local } Axiom {+ ( {+ @ident } : @type ) }
-             {? Local } Axioms {+ ( {+ @ident } : @type ) }
-             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
-             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
+   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
+             {? Local } Axiom {+ ( {+ @ident } : @type ) }
+             {? Local } Axioms {+ ( {+ @ident } : @type ) }
+             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
+             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
       :name: Parameters; Axiom; Axioms; Conjecture; Conjectures
 
-      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
+      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
-             Variables {+ ( {+ @ident } : @type ) }
-             Hypothesis {+ ( {+ @ident } : @type ) }
-             Hypotheses {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
       :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
       Outside of any section, these variants are synonyms of
-      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
       For their meaning inside a section, see :cmd:`Variable` in
       :ref:`section-mechanism`.
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index a7eb7c2319..bbd7e0ba3d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -360,7 +360,7 @@ Detecting progress
 
 We can check if a tactic made progress with:
 
-.. tacn:: progress expr
+.. tacn:: progress @expr
    :name: progress
 
    :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v``
@@ -555,7 +555,7 @@ Identity
 The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but
 it appears in the proof script.
 
-.. tacn:: idtac {* message_token}
+.. tacn:: idtac {* @message_token}
    :name: idtac
 
    This prints the given tokens. Strings and integers are printed
@@ -684,7 +684,7 @@ Timing a tactic that evaluates to a term
 Tactic expressions that produce terms can be timed with the experimental
 tactic
 
-.. tacn:: time_constr expr
+.. tacn:: time_constr @expr
    :name: time_constr
 
    which evaluates :n:`@expr ()` and displays the time the tactic expression
@@ -880,7 +880,7 @@ We can perform pattern matching on goals using the following expression:
 
 .. we should provide the full grammar here
 
-.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
    :name: match goal
 
    If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is
@@ -918,7 +918,7 @@ We can perform pattern matching on goals using the following expression:
       first), but it possible to reverse this order (oldest first)
       with the :n:`match reverse goal with` variant.
 
-   .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+   .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
 
       Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics
       to backtrack into a right-hand side tactic which has backtracking points
@@ -929,7 +929,7 @@ We can perform pattern matching on goals using the following expression:
       The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for
       :n:`once multimatch [reverse] goal …`.
 
-   .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+   .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
 
       Using lazymatch instead of match will perform the same pattern matching
       procedure but will commit to the first matching branch with the first
@@ -1135,33 +1135,33 @@ Defining |Ltac| functions
 
 Basically, |Ltac| toplevel definitions are made as follows:
 
-.. cmd:: Ltac @ident {* @ident} := @expr
+.. cmd:: {? Local} Ltac @ident {* @ident} := @expr
+   :name: Ltac
 
    This defines a new |Ltac| function that can be used in any tactic
    script or new |Ltac| toplevel definition.
 
+   If preceded by the keyword ``Local``, the tactic definition will not be
+   exported outside the current module.
+
    .. note::
 
       The preceding definition can equivalently be written:
 
       :n:`Ltac @ident := fun {+ @ident} => @expr`
 
-   Recursive and mutual recursive function definitions are also possible
-   with the syntax:
-
    .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr
 
-      It is also possible to *redefine* an existing user-defined tactic using the syntax:
+      This syntax allows recursive and mutual recursive function definitions.
 
    .. cmdv:: Ltac @qualid {* @ident} ::= @expr
 
+      This syntax *redefines* an existing user-defined tactic.
+
       A previous definition of qualid must exist in the environment. The new
       definition will always be used instead of the old one and it goes across
       module boundaries.
 
-   If preceded by the keyword Local the tactic definition will not be
-   exported outside the current module.
-
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 139506723e..4a2f9c0db3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -544,9 +544,9 @@ Requesting information
 
       ``<Your Tactic Text here>``.
 
-     .. deprecated:: 8.10
+      .. deprecated:: 8.10
 
-        Please use a text editor.
+         Please use a text editor.
 
    .. cmdv:: Show Proof
       :name: Show Proof
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index d6247d1bc5..75e019592f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic:
 An alternative use of the ``have`` tactic is to provide the explicit proof
 term for the intermediate lemma, using tactics of the form:
 
-.. tacv:: have {? @ident } := term
+.. tacv:: have {? @ident } := @term
 
    This tactic creates a new assumption of type the type of :token:`term`.
    If the
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 537a40c53c..4e47621938 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``,
       and ``in`` clauses.
 
-.. tacn:: case term
+.. tacn:: case @term
    :name: case
 
    The tactic :n:`case` is a more basic tactic to perform case analysis without
@@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`induction @ident; induction @ident` (or
    :n:`induction @ident ; destruct @ident` depending on the exact needs).
 
-.. tacv:: double induction num1 num2
+.. tacv:: double induction @num__1 @num__2
 
    This tactic is deprecated and should be replaced by
    :n:`induction num1; induction num3` where :n:`num3` is the result
@@ -2271,11 +2271,11 @@ and an explanation of the underlying technique.
          :undocumented:
 
    .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern}
-             injection @num as {+ simple_intropattern}
-             injection as {+ simple_intropattern}
-             einjection @term {? with @bindings_list} as {+ simple_intropattern}
-             einjection @num as {+ simple_intropattern}
-             einjection as {+ simple_intropattern}
+             injection @num as {+ @simple_intropattern}
+             injection as {+ @simple_intropattern}
+             einjection @term {? with @bindings_list} as {+ @simple_intropattern}
+             einjection @num as {+ @simple_intropattern}
+             einjection as {+ @simple_intropattern}
 
       These variants apply :n:`intros {+ @simple_intropattern}` after the call to
       :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
@@ -2637,7 +2637,7 @@ and an explanation of the underlying technique.
    is correct at some time of the interactive development of a proof, use
    the command ``Guarded`` (see Section :ref:`requestinginformation`).
 
-.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)}
+.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)}
 
    This starts a proof by mutual induction. The statements to be simultaneously
    proved are respectively :g:`forall binder ... binder, type`.
@@ -4048,7 +4048,7 @@ Setting implicit automation tactics
    .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`.
 
 
-   .. cmdv:: Proof with tactic using {+ @ident}
+   .. cmdv:: Proof with @tactic using {+ @ident}
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
@@ -4400,6 +4400,11 @@ Equality
    This tactic applies to a goal that has the form :g:`t=u` and transforms it
    into the two subgoals :n:`t=@term` and :n:`@term=u`.
 
+   .. tacv:: etransitivity
+
+      This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of
+      a concrete :token:`term`.
+
 
 Equality and inductive sets
 ---------------------------
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 4e4a10f590..26dc4e02cf 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -277,7 +277,7 @@ Requests to the environment
       :token:`term_pattern` (holes of the pattern are either denoted by `_` or by
       :n:`?@ident` when non linear patterns are expected).
 
-   .. cmdv:: Search { + [-]@term_pattern_string }
+   .. cmdv:: Search {+ {? -}@term_pattern_string}
 
       where
       :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
@@ -289,17 +289,17 @@ Requests to the environment
       prefixed by `-`, the search excludes the objects that mention that
       term_pattern or that string.
 
-   .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
+   .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid }
 
       This restricts the search to constructions defined in the modules
       named by the given :n:`qualid` sequence.
 
-   .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
+   .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid }
 
       This restricts the search to constructions not defined in the modules
       named by the given :n:`qualid` sequence.
 
-   .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
+   .. cmdv:: @selector: Search {+ {? -}@term_pattern_string}
 
       This specifies the goal on which to search hypothesis (see
       Section :ref:`invocation-of-tactics`).
@@ -353,7 +353,7 @@ Requests to the environment
       This restricts the search to constructions defined in the modules named
       by the given :n:`qualid` sequence.
 
-   .. cmdv:: SearchHead term outside {+ @qualid }
+   .. cmdv:: SearchHead @term outside {+ @qualid }
 
       This restricts the search to constructions not defined in the modules
       named by the given :n:`qualid` sequence.
@@ -443,7 +443,7 @@ Requests to the environment
 
          SearchRewrite (_ + _ + _).
 
-   .. cmdv:: SearchRewrite term inside {+ @qualid }
+   .. cmdv:: SearchRewrite @term inside {+ @qualid }
 
       This restricts the search to constructions defined in the modules
       named by the given :n:`qualid` sequence.
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 418922e9b3..3a12ee288a 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme``
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
-.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort
+.. cmd:: Derive Inversion @ident with @ident Sort @sort
+         Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    This command generates an inversion principle for the
-   :tacn:`inversion ... using ...`  tactic. Let :g:`I` be an inductive
-   predicate and :g:`x` the variables occurring in t. This command
-   generates and stocks the inversion lemma for the sort :g:`sort`
-   corresponding to the instance :g:`∀ (x:T), I t` with the name
-   :n:`@ident` in the global environment. When applied, it is
-   equivalent to having inverted the instance with the tactic
-   :g:`inversion`.
-
+   :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
+   :token:`term`. This command generates the inversion lemma for the sort
+   :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+   When applied, it is equivalent to having inverted the instance with the
+   tactic :g:`inversion`.
 
-.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
+          Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
-.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
+          Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
-.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
+          Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index edec13f681..cda228a7da 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -327,22 +327,29 @@ symbols.
 Reserving notations
 ~~~~~~~~~~~~~~~~~~~
 
-A given notation may be used in different contexts. Coq expects all
-uses of the notation to be defined at the same precedence and with the
-same associativity. To avoid giving the precedence and associativity
-every time, it is possible to declare a parsing rule in advance
-without giving its interpretation. Here is an example from the initial
-state of Coq.
+.. cmd:: Reserved Notation @string {? (@modifiers) }
 
-.. coqtop:: in
+   A given notation may be used in different contexts. Coq expects all
+   uses of the notation to be defined at the same precedence and with the
+   same associativity. To avoid giving the precedence and associativity
+   every time, this command declares a parsing rule (:token:`string`) in advance
+   without giving its interpretation. Here is an example from the initial
+   state of Coq.
+
+   .. coqtop:: in
+
+      Reserved Notation "x = y" (at level 70, no associativity).
+
+   Reserving a notation is also useful for simultaneously defining an
+   inductive type or a recursive constant and a notation for it.
 
-   Reserved Notation "x = y" (at level 70, no associativity).
+   .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
+             their precedence and associativity cannot be changed.
 
-Reserving a notation is also useful for simultaneously defining an
-inductive type or a recursive constant and a notation for it.
+   .. cmdv:: Reserved Infix "@symbol" {* @modifiers}
 
-.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
-          their precedence and associativity cannot be changed.
+      This command declares an infix parsing rule without giving its
+      interpretation.
 
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~