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

Reviewed-by: Zimmi48

2 files changed, 23 insertions, 22 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