Merge PR #13343: Update syntax in auto.rst chapter

Reviewed-by: Zimmi48
Ack-by: JasonGross

3 files changed, 15 insertions, 11 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 27ae7cea3a..039a23e8c2 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -535,11 +535,19 @@ pass additional arguments such as ``using relation``.
 .. tacn:: setoid_reflexivity
           setoid_symmetry {? in @ident }
           setoid_transitivity @one_term
-          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident }
-          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @rewrite_occs } {? in @ident }
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @rewrite_occs
           setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 }
    :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace
 
+   .. todo: move rewrite_occs to rewrite chapter when that chapter is revised
+
+   .. insertprodn rewrite_occs rewrite_occs
+
+   .. prodn::
+      rewrite_occs ::= {+ @integer }
+      | @ident
+
    The ``using relation`` arguments cannot be passed to the unprefixed form.
    The latter argument tells the tactic what parametric relation should
    be used to replace the first tactic argument with the second one. If
@@ -714,6 +722,8 @@ instances are tried at each node of the search tree). To speed it up,
 declare your constant as rigid for proof search using the command
 :cmd:`Typeclasses Opaque`.
 
+.. _strategies4rewriting:
+
 Strategies for rewriting
 ------------------------
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 98445fca1a..4143d836c4 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -335,12 +335,6 @@ Summary of the commands
 
 .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } }
 
-   .. insertprodn hint_info one_pattern
-
-   .. prodn::
-      hint_info ::= %| {? @natural } {? @one_pattern }
-      one_pattern ::= @one_term
-
    Declares a typeclass instance named
    :token:`ident_decl` of the class :n:`@type` with the specified parameters and with
    fields defined by :token:`field_def`, where each field must be a declared field of
@@ -503,7 +497,7 @@ Typeclasses Transparent, Typeclasses Opaque
 
    It is useful when some constants prevent some unifications and make
    resolution fail. It is also useful to declare constants which
-   should never be unfolded during proof-search, like fixpoints or
+   should never be unfolded during proof search, like fixpoints or
    anything which does not look like an abbreviation. This can
    additionally speed up proof search as the typeclass map can be
    indexed by such rigid constants (see
@@ -555,7 +549,7 @@ Settings
       This can be expensive as it requires rebuilding hint
       clauses dynamically, and does not benefit from the invertibility
       status of the product introduction rule, resulting in potentially more
-      expensive proof-search (i.e. more useless backtracking).
+      expensive proof search (i.e. more useless backtracking).
 
 .. flag:: Typeclass Resolution For Conversion
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 4615a8dfca..bb78b142ca 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -412,7 +412,7 @@ Explicit Universes
    | _
    | @qualid
    univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
-   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
    univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 The syntax has been extended to allow users to explicitly bind names