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

Reviewed-by: Zimmi48
Ack-by: JasonGross

2 files changed, 319 insertions, 387 deletions

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index cc4ab76502..472df2bd91 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -4,104 +4,87 @@
 Programmable proof search
 =========================
 
-.. tacn:: auto
-   :name: auto
+.. tacn:: auto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
-   This tactic implements a Prolog-like resolution procedure to solve the
+   .. insertprodn auto_using hintbases
+
+   .. prodn::
+      auto_using ::= using {+, @one_term }
+      hintbases ::= with *
+      | with {+ @ident }
+
+   Implements a Prolog-like resolution procedure to solve the
    current goal. It first tries to solve the goal using the :tacn:`assumption`
    tactic, then it reduces the goal to an atomic one using :tacn:`intros` and
    introduces the newly generated hypotheses as hints. Then it looks at
-   the list of tactics associated to the head symbol of the goal and
-   tries to apply one of them (starting from the tactics with lower
-   cost). This process is recursively applied to the generated subgoals.
+   the list of tactics associated with the head symbol of the goal and
+   tries to apply one of them.  Lower cost tactics are tried before higher-cost
+   tactics.  This process is recursively applied to the generated subgoals.
 
-   By default, :tacn:`auto` only uses the hypotheses of the current goal and
-   the hints of the database named ``core``.
+   :n:`@nat_or_var`
+     Specifies the maximum search depth.  The default is 5.
 
-   .. warning::
+   :n:`using {+, @one_term }`
 
-      :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to
-      :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will
-      fail even if applying manually one of the hints would succeed.
+      Uses lemmas :n:`{+, @one_term }` in addition to hints. If :n:`@one_term` is an
+      inductive type, the collection of its constructors are added as hints.
 
-   .. tacv:: auto @natural
+      Note that hints passed through the `using` clause are used in the same
+      way as if they were passed through a hint database. Consequently,
+      they use a weaker version of :tacn:`apply` and :n:`auto using @one_term`
+      may fail where :n:`apply @one_term` succeeds.
 
-      Forces the search depth to be :token:`natural`. The maximal search depth
-      is 5 by default.
+      .. todo
+         Given that this can be seen as counter-intuitive, it could be useful
+         to have an option to use full-blown :tacn:`apply` for lemmas passed
+         through the `using` clause. Contributions welcome!
 
-   .. tacv:: auto with {+ @ident}
+   :n:`with *`
+     Use all existing hint databases. Using this variant is highly discouraged
+     in finished scripts since it is both slower and less robust than explicitly
+     selecting the required databases.
 
-      Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``.
+   :n:`with {+ @ident }`
+     Use the hint databases :n:`{+ @ident}` in addition to the database ``core``.
+     Use the fake database `nocore` to omit `core`.
 
-      .. note::
+   If no `with` clause is given, :tacn:`auto` only uses the hypotheses of the
+   current goal and the hints of the database named ``core``.
 
-         Use the fake database `nocore` if you want to *not* use the `core`
-         database.
+   :tacn:`auto` generally either completely solves the goal or
+   leaves it unchanged.  Use :tacn:`solve` `[ auto ]` if you want a failure
+   when they don't solve the goal.  :tacn:`auto` will fail if :tacn:`fail`
+   or :tacn:`gfail` are invoked directly or indirectly, in which case setting
+   the :flag:`Ltac Debug` may help you debug the failure.
 
-   .. tacv:: auto with *
+   .. warning::
 
-      Uses all existing hint databases. Using this variant is highly discouraged
-      in finished scripts since it is both slower and less robust than the variant
-      where the required databases are explicitly listed.
+      :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to
+      :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will
+      fail even if applying manually one of the hints would succeed.
 
    .. seealso::
-      :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
+      :ref:`thehintsdatabasesforautoandeauto` for the list of
       pre-defined databases and the way to create or extend a database.
 
-   .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } }
-
-      Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an
-      inductive type, it is the collection of its constructors which are added
-      as hints.
-
-      .. note::
-
-         The hints passed through the `using` clause are used in the same
-         way as if they were passed through a hint database. Consequently,
-         they use a weaker version of :tacn:`apply` and :n:`auto using @qualid`
-         may fail where :n:`apply @qualid` succeeds.
-
-         Given that this can be seen as counter-intuitive, it could be useful
-         to have an option to use full-blown :tacn:`apply` for lemmas passed
-         through the `using` clause. Contributions welcome!
-
-   .. tacv:: info_auto
+   .. tacn:: info_auto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
       Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This
       variant is very useful for getting a better understanding of automation, or
       to know what lemmas/assumptions were used.
 
-   .. tacv:: debug auto
-      :name: debug auto
+   .. tacn:: debug auto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
       Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
       including failing paths.
 
-   .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}}
-
-      This is the most general form, combining the various options.
-
-.. tacv:: trivial
-   :name: trivial
-
-   This tactic is a restriction of :tacn:`auto` that is not recursive
-   and tries only hints that cost `0`. Typically it solves trivial
-   equalities like :g:`X=X`.
-
-   .. tacv:: trivial with {+ @ident}
-             trivial with *
-             trivial using {+ @qualid}
-             debug trivial
-             info_trivial
-             {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}}
-      :name: _; _; _; debug trivial; info_trivial; _
-      :undocumented:
+.. tacn:: trivial {? @auto_using } {? @hintbases }
+          debug trivial {? @auto_using } {? @hintbases }
+          info_trivial {? @auto_using } {? @hintbases }
 
-.. note::
-  :tacn:`auto` and :tacn:`trivial` either solve completely the goal or
-  else succeed without changing the goal. Use :g:`solve [ auto ]` and
-  :g:`solve [ trivial ]` if you would prefer these tactics to fail when
-  they do not manage to solve the goal.
+   Like :tacn:`auto`, but is not recursive
+   and only tries hints with zero cost. Typically used to solve goals
+   for which a lemma is already available in the specified :n:`hintbases`.
 
 .. flag:: Info Auto
           Debug Auto
@@ -111,10 +94,9 @@ Programmable proof search
    These flags enable printing of informative or debug information for
    the :tacn:`auto` and :tacn:`trivial` tactics.
 
-.. tacn:: eauto
-   :name: eauto
+.. tacn:: eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
-   This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try
+   Generalizes :tacn:`auto`. While :tacn:`auto` does not try
    resolution hints which would leave existential variables in the goal,
    :tacn:`eauto` does try them (informally speaking, it internally uses a tactic
    close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply`
@@ -133,12 +115,13 @@ Programmable proof search
          Goal forall P:nat -> Prop, P 0 -> exists n, P n.
          eauto.
 
-      Note that ``ex_intro`` should be declared as a hint.
+      `ex_intro` is declared as a hint so the proof succeeds.
 
+   .. seealso:: :ref:`thehintsdatabasesforautoandeauto`
 
-   .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}}
+   .. tacn:: info_eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
-      The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
+      The various options for :tacn:`info_eauto` are the same as for :tacn:`info_auto`.
 
    :tacn:`eauto` also obeys the following flags:
 
@@ -146,34 +129,55 @@ Programmable proof search
              Debug Eauto
       :undocumented:
 
-   .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
+   .. tacn:: debug eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
+      Behaves like :tacn:`eauto` but shows the tactics it tries to solve the goal,
+      including failing paths.
+
+   .. tacn:: bfs eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
+
+      Like :tacn:`eauto`, but uses a
+      `breadth-first search <https://en.wikipedia.org/wiki/Breadth-first_search>`_.
 
-.. tacn:: autounfold with {+ @ident}
-   :name: autounfold
+.. tacn:: autounfold {? @hintbases } {? @occurrences }
 
-   This tactic unfolds constants that were declared through a :cmd:`Hint Unfold`
+   Unfolds constants that were declared through a :cmd:`Hint Unfold`
    in the given databases.
 
-.. tacv:: autounfold with {+ @ident} in @goal_occurrences
+   :n:`@occurrences`
+     Performs the unfolding in the specified occurrences.  The :n:`at @occs_nums`
+     clause of :n:`@occurrences` is not supported.
+
+.. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr }
+
+   `*`
+     If present, rewrite all occurrences whose side conditions are solved.
 
-   Performs the unfolding in the given clause (:token:`goal_occurrences`).
+     .. todo: This may not always work as described, see #4976 #7672 and
+        https://github.com/coq/coq/issues/1933#issuecomment-337497938 as
+        mentioned here: https://github.com/coq/coq/pull/13343#discussion_r527801604
 
-.. tacv:: autounfold with *
+   :n:`with {+ @ident }`
+     Specifies the rewriting rule bases to use.
 
-   Uses the unfold hints declared in all the hint databases.
+   :n:`@occurrences`
+     Performs rewriting in the specified occurrences.  Note: the `at` clause
+     is currently not supported.
 
-.. tacn:: autorewrite with {+ @ident}
-   :name: autorewrite
+     .. exn:: The "at" syntax isn't available yet for the autorewrite tactic.
 
-   This tactic carries out rewritings according to the rewriting rule
-   bases :n:`{+ @ident}`.
+        Appears when there is an `at` clause on the conclusion.
 
-   Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
+   :n:`using @ltac_expr`
+     :token:`ltac_expr` is applied to the main subgoal after each rewriting step.
+
+   Applies rewritings according to the rewriting rule bases :n:`{+ @ident }`.
+
+   For each rule base, applies each rewriting to the main subgoal until
    it fails. Once all the rules have been processed, if the main subgoal has
-   progressed (e.g., if it is distinct from the initial main goal) then the rules
-   of this base are processed again. If the main subgoal has not progressed then
-   the next base is processed. For the bases, the behavior is exactly similar to
+   changed then the rules
+   of this base are processed again. If the main subgoal has not changed then
+   the next base is processed. For the bases, the behavior is very similar to
    the processing of the rewriting rules.
 
    The rewriting rule bases are built with the :cmd:`Hint Rewrite`
@@ -183,31 +187,13 @@ Programmable proof search
 
    This tactic may loop if you build non terminating rewriting systems.
 
-.. tacv:: autorewrite with {+ @ident} using @tactic
-
-  Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}`
-  applying tactic to the main subgoal after each rewriting step.
-
-.. tacv:: autorewrite with {+ @ident} in @qualid
-
-   Performs all the rewritings in hypothesis :n:`@qualid`.
-
-.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic
-
-  Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic`
-  to the main subgoal after each rewriting step.
-
-.. tacv:: autorewrite with {+ @ident} in @goal_occurrences
-
-  Performs all the rewriting in the clause :n:`@goal_occurrences`.
-
 .. seealso::
 
-   :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by
+   :cmd:`Hint Rewrite` for feeding the database of lemmas used by
    :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic.
+   Also see :ref:`strategies4rewriting`.
 
 .. tacn:: easy
-   :name: easy
 
    This tactic tries to solve the current goal by a number of standard closing steps.
    In particular, it tries to close the current goal using the closing tactics
@@ -220,45 +206,43 @@ Programmable proof search
    This tactic solves goals that belong to many common classes; in particular, many cases of
    unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic.
 
-.. tacv:: now @tactic
-   :name: now
+.. tacn:: now @ltac_expr
 
    Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`.
 
-Controlling automation
---------------------------
-
 .. _thehintsdatabasesforautoandeauto:
 
 The hints databases for auto and eauto
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--------------------------------------
 
 The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database
-maps head symbols to a list of hints.
-
-.. cmd:: Print Hint @ident
+maps head symbols to a list of hints.  Use the :cmd:`Print Hint` command to view
+the database.
 
-   Use this command
-   to display the hints associated to the head symbol :n:`@ident`
-   (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
-   integer, and an optional pattern. The hints with lower cost are tried first. A
-   hint is tried by :tacn:`auto` when the conclusion of the current goal matches its
-   pattern or when it has no pattern.
+Each hint has a cost that is a nonnegative
+integer and an optional pattern. Hints with lower costs are tried first.
+:tacn:`auto` tries a hint when the conclusion of the current goal matches its
+pattern or when the hint has no pattern.
 
 Creating Hint databases
-```````````````````````
+-----------------------
 
-One can optionally declare a hint database using the command
-:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be
-automatically created.
+Hint databases can be created with the :cmd:`Create HintDb` command or implicitly
+by adding a hint to an unknown database.  We recommend you always use :cmd:`Create HintDb`
+and then imediately use :cmd:`Hint Constants` and :cmd:`Hint Variables` to make
+those settings explicit.
 
-.. cmd:: Create HintDb @ident {? discriminated}
+Note that the default transparency
+settings differ between these two methods of creation.  Databases created with
+:cmd:`Create HintDb` have the default setting `Transparent` for both `Variables`
+and `Constants`, while implicitly created databases have the `Opaque` setting.
 
-   This command creates a new database named :n:`@ident`. The database is
+.. cmd:: Create HintDb @ident {? discriminated }
+
+   Creates a new hint database named :n:`@ident`. The database is
    implemented by a Discrimination Tree (DT) that serves as an index of
    all the lemmas. The DT can use transparency information to decide if a
    constant should be indexed or not
-   (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
    making the retrieval more efficient. The legacy implementation (the default one
    for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto`
    goals), for non-Immediate hints and does not make use of transparency
@@ -270,149 +254,144 @@ automatically created.
    from the order in which they were inserted, making this implementation
    observationally different from the legacy one.
 
-.. cmd:: Hint @hint_definition : {+ @ident}
+.. _creating_hints:
+
+Creating Hints
+--------------
 
-   The general command to add a hint to some databases :n:`{+ @ident}`.
+   The various `Hint` commands share these elements:
 
-   This command supports the :attr:`local`, :attr:`global` and :attr:`export`
-   locality attributes. When no locality is explictly given, the
-   command is :attr:`local` inside a section and :attr:`global` otherwise.
+   :n:`{? : {+ @ident } }` specifies the hint database(s) to add to.
+   *(Deprecated since version 8.10:* If no :token:`ident`\s
+   are given, the hint is added to the `core` database.)
+
+   Outside of sections, these commands support the :attr:`local`, :attr:`export`
+   and :attr:`global` attributes. :attr:`global` is the default.  Inside sections,
+   only the :attr:`local` attribute is supported because hints are local to sections.
 
    + :attr:`local` hints are never visible from other modules, even if they
-     require or import the current module. Inside a section, the :attr:`local`
-     attribute is useless since hints do not survive anyway to the closure of
-     sections.
+     :cmd:`Import` or :cmd:`Require` the current module.
 
-   + :attr:`export` are visible from other modules when they import the current
-     module. Requiring it is not enough.
+   + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current
+     module, but not when they only :cmd:`Require` it. This attribute is supported by
+     all `Hint` commands except for :cmd:`Hint Rewrite`.
 
-   + :attr:`global` hints are made available by merely requiring the current
-     module.
+   + :attr:`global` hints are visible from other modules when they :cmd:`Import` or
+     :cmd:`Require` the current module.
 
    .. deprecated:: 8.13
 
-     The default value for hint locality is scheduled to change in a future
+     The default value for hint locality will change in a future
      release. For the time being, adding hints outside of sections without
-     specifying an explicit locality is therefore triggering a deprecation
-     warning. It is recommended to use :attr:`export` whenever possible
-
-   The various possible :production:`hint_definition`\s are given below.
-
-   .. cmdv:: Hint @hint_definition
+     specifying an explicit locality will trigger a deprecation
+     warning. We recommend you use :attr:`export` whenever possible.
 
-      No database name is given: the hint is registered in the ``core`` database.
+   The `Hint` commands are:
 
-      .. deprecated:: 8.10
+   .. cmd:: Hint Resolve {+ {| @qualid | @one_term } } {? @hint_info } {? : {+ @ident } }
+            Hint Resolve {| -> | <- } {+ @qualid } {? @natural } {? : {+ @ident } }
+      :name: Hint Resolve; _
 
-   .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident
-      :name: Hint Resolve
+      .. insertprodn hint_info one_pattern
 
-      This command adds :n:`simple apply @qualid` to the hint list with the head
-      symbol of the type of :n:`@qualid`. The cost of that hint is the number of
-      subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The
-      associated :n:`@pattern` is inferred from the conclusion of the type of
-      :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type
-      of :n:`@qualid` does not start with a product the tactic added in the hint list
-      is :n:`exact @qualid`. In case this type can however be reduced to a type
-      starting with a product, the tactic :n:`simple apply @qualid` is also stored in
-      the hints list. If the inferred type of :n:`@qualid` contains a dependent
-      quantification on a variable which occurs only in the premisses of the type
+      .. prodn::
+         hint_info ::= %| {? @natural } {? @one_pattern }
+         one_pattern ::= @one_term
+
+      The first form adds each :n:`@qualid` as a hint with the head symbol of the type of
+      :n:`@qualid` to the specified hint databases (:n:`@ident`\s). The cost of the hint is the number of
+      subgoals generated by :tacn:`simple apply` :n:`@qualid` or, if specified, :n:`@natural`. The
+      associated pattern is inferred from the conclusion of the type of
+      :n:`@qualid` or, if specified, the given :n:`@one_pattern`.
+
+      If the inferred type
+      of :n:`@qualid` does not start with a product, :tacn:`exact` :n:`@qualid` is added
+      to the hint list.  If the type can be reduced to a type starting with a product,
+      :tacn:`simple apply` :n:`@qualid` is also added to the hints list.
+
+      If the inferred type of :n:`@qualid` contains a dependent
+      quantification on a variable which occurs only in the premises of the type
       and not in its conclusion, no instance could be inferred for the variable by
-      unification with the goal. In this case, the hint is added to the hint list
-      of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
-      typical example of a hint that is used only by :tacn:`eauto` is a transitivity
+      unification with the goal. In this case, the hint is only used by
+      :tacn:`eauto` / :tacn:`typeclasses eauto`, but not by :tacn:`auto`.  A
+      typical hint that would only be used by :tacn:`eauto` is a transitivity
       lemma.
 
-      .. exn:: @qualid cannot be used as a hint
-
-         The head symbol of the type of :n:`@qualid` is a bound variable
-         such that this tactic cannot be associated to a constant.
-
-   .. cmdv:: Hint Resolve {+ @qualid} : @ident
+      :n:`{| -> | <- }`
+        The second form adds the left-to-right (`->`) or right-ot-left implication (`<-`)
+        of an equivalence as a hint (informally
+        the hint will be used as, respectively, :tacn:`apply` :n:`-> @qualid` or
+        :tacn:`apply` :n:`<- @qualid`,
+        although as mentioned before, the tactic actually used is a restricted version of
+        :tacn:`apply`).
 
-      Adds each :n:`Hint Resolve @qualid`.
+      :n:`@one_term`
+        Permits declaring a hint without declaring a new
+        constant first, but this is not recommended.
 
-   .. cmdv:: Hint Resolve -> @qualid : @ident
+         .. warn:: Declaring arbitrary terms as hints is fragile; it is recommended to declare a toplevel constant instead
+            :undocumented:
 
-      Adds the left-to-right implication of an equivalence as a hint (informally
-      the hint will be used as :n:`apply <- @qualid`, although as mentioned
-      before, the tactic actually used is a restricted version of
-      :tacn:`apply`).
-
-   .. cmdv:: Hint Resolve <- @qualid
+      .. exn:: @qualid cannot be used as a hint
 
-      Adds the right-to-left implication of an equivalence  as a hint.
+         The head symbol of the type of :n:`@qualid` is a bound variable
+         such that this tactic cannot be associated to a constant.
 
-   .. cmdv:: Hint Immediate @qualid : @ident
-      :name: Hint Immediate
+   .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } }
 
-      This command adds :n:`simple apply @qualid; trivial` to the hint list associated
-      with the head symbol of the type of :n:`@ident` in the given database. This
-      tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are
+      Adds :tacn:`simple apply` :n:`@qualid;` :tacn:`trivial` to the hint list for each :n:`@qualid` associated
+      with the head symbol of the type of :n:`@ident`. This
+      tactic will fail if all the subgoals generated by :tacn:`simple apply` :n:`@qualid` are
       not solved immediately by the :tacn:`trivial` tactic (which only tries tactics
-      with cost 0).This command is useful for theorems such as the symmetry of
-      equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited
-      use in order to avoid useless proof-search. The cost of this tactic (which
+      with cost 0). This command is useful for theorems such as the symmetry of
+      equality or :g:`n+1=m+1 -> n=m` that we may want to introduce with limited
+      use in order to avoid useless proof search. The cost of this tactic (which
       never generates subgoals) is always 1, so that it is not used by :tacn:`trivial`
       itself.
 
-   .. exn:: @qualid cannot be used as a hint
-      :undocumented:
+   .. cmd:: Hint Constructors {+ @qualid } {? : {+ @ident } }
 
-   .. cmdv:: Hint Immediate {+ @qualid} : @ident
-
-      Adds each :n:`Hint Immediate @qualid`.
-
-   .. cmdv:: Hint Constructors @qualid : @ident
-      :name: Hint Constructors
-
-      If :token:`qualid` is an inductive type, this command adds all its constructors as
+      For each :n:`@qualid` that is an inductive type, adds all its constructors as
       hints of type ``Resolve``. Then, when the conclusion of current goal has the form
       :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor.
 
       .. exn:: @qualid is not an inductive type
          :undocumented:
 
-   .. cmdv:: Hint Constructors {+ @qualid} : @ident
-
-      Extends the previous command for several inductive types.
+   .. cmd:: Hint Unfold {+ @qualid } {? : {+ @ident } }
 
-   .. cmdv:: Hint Unfold @qualid : @ident
-      :name: Hint Unfold
-
-      This adds the tactic :n:`unfold @qualid` to the hint list that will only be
-      used when the head constant of the goal is :token:`qualid`.
+      For each :n:`@qualid`, adds the tactic :tacn:`unfold` :n:`@qualid` to the
+      hint list that will only be used when the head constant of the goal is :token:`qualid`.
       Its cost is 4.
 
-   .. cmdv:: Hint Unfold {+ @qualid}
-
-      Extends the previous command for several defined constants.
-
-   .. cmdv:: Hint Transparent {+ @qualid} : @ident
-             Hint Opaque {+ @qualid} : @ident
+   .. cmd:: Hint {| Transparent | Opaque } {+ @qualid } {? : {+ @ident } }
       :name: Hint Transparent; Hint Opaque
 
-      This adds transparency hints to the database, making :n:`@qualid`
-      transparent or opaque constants during resolution. This information is used
+      Adds transparency hints to the database, making each :n:`@qualid`
+      a transparent or opaque constant during resolution. This information is used
       during unification of the goal with any lemma in the database and inside the
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-   .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident
-             Hint Constants {| Transparent | Opaque } : @ident
-      :name: Hint Variables; Hint Constants
+   .. cmd:: Hint {| Constants | Variables } {| Transparent | Opaque } {? : {+ @ident } }
+      :name: Hint Constants; Hint Variables
 
-      This sets the transparency flag used during unification of
-      hints in the database for all constants or all variables,
-      overwriting the existing settings of opacity. It is advised
-      to use this just after a :cmd:`Create HintDb` command.
+      Sets the transparency flag for constants or variables for the specified hint
+      databases.
+      These flags affect the unification of hints in the database.
+      We advise using this just after a :cmd:`Create HintDb` command.
 
-   .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident
-      :name: Hint Extern
+   .. cmd:: Hint Extern @natural {? @one_pattern } => @ltac_expr {? : {+ @ident } }
 
-      This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
-      :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
-      :n:`@tactic` to execute.
+      Extends :tacn:`auto` with tactics other than :tacn:`apply` and
+      :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_term` is the pattern
+      to match and :n:`@ltac_expr` is the action to apply.
+
+      .. note::
+
+         Use a :cmd:`Hint Extern` with no pattern to do
+         pattern matching on hypotheses using ``match goal with``
+         inside the tactic.
 
       .. example::
 
@@ -441,80 +420,131 @@ automatically created.
          .. coqtop:: all
 
             Require Import List.
-            Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
+            Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) =>
+              generalize  X1, X2; decide equality : eqdec.
             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
-            Info 1 auto with eqdec.
+            info_auto.
 
-   .. cmdv:: Hint Cut @regexp : @ident
-      :name: Hint Cut
+   .. cmd:: Hint Cut [ @hints_regexp ] {? : {+ @ident } }
 
-      .. warning::
-
-         These hints currently only apply to typeclass proof search and the
-         :tacn:`typeclasses eauto` tactic.
-
-      This command can be used to cut the proof-search tree according to a regular
-      expression matching paths to be cut. The grammar for regular expressions is
-      the following. Beware, there is no operator precedence during parsing, one can
-      check with :cmd:`Print HintDb` to verify the current cut expression:
+      .. DISABLED insertprodn hints_regexp hints_regexp
 
       .. prodn::
-         regexp ::= @ident   (hint or instance identifier)
+         hints_regexp ::= {+ @qualid }   (hint or instance identifier)
          | _   (any hint)
-         | @regexp | @regexp   (disjunction)
-         | @regexp @regexp   (sequence)
-         | @regexp *   (Kleene star)
+         | @hints_regexp | @hints_regexp   (disjunction)
+         | @hints_regexp @hints_regexp   (sequence)
+         | @hints_regexp *   (Kleene star)
          | emp   (empty)
          | eps   (epsilon)
-         | ( @regexp )
+         | ( @hints_regexp )
+
+      Used to cut the proof search tree according to a regular
+      expression that matches the paths to be cut.
+
 
-      The `emp` regexp does not match any search path while `eps`
-      matches the empty path. During proof search, the path of
-      successive successful hints on a search branch is recorded, as a
-      list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have
+      During proof search, the path of
+      successive successful hints on a search branch is recorded as a
+      list of identifiers for the hints (note that :cmd:`Hint Extern`\s do not have
       an associated identifier).
-      Before applying any hint :n:`@ident` the current path `p` extended with
-      :n:`@ident` is matched against the current cut expression `c` associated to
-      the hint database. If matching succeeds, the hint is *not* applied. The
-      semantics of :n:`Hint Cut @regexp` is to set the cut expression
-      to :n:`c | regexp`, the initial cut expression being `emp`.
-
-   .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident
-      :name: Hint Mode
-
-      This sets an optional mode of use of the identifier :n:`@qualid`. When
-      proof-search faces a goal that ends in an application of :n:`@qualid` to
-      arguments :n:`@term ... @term`, the mode tells if the hints associated to
-      :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
+      For each hint :n:`@qualid` in the hint database, the current path `p`
+      extended with :n:`@qualid`
+      is matched against the current cut expression `c` associated with the
+      hint database.  If the match succeeds the hint is *not* applied.
+
+      :n:`Hint Cut @hints_regexp` sets the cut expression
+      to :n:`c | @hints_regexp`.  The initial cut expression is `emp`.
+
+      The output of :cmd:`Print HintDb` shows the cut expression.
+
+      .. warning::
+
+         There is no operator precedence during parsing, one can
+         check with :cmd:`Print HintDb` to verify the current cut expression.
+
+      .. warning::
+
+         These hints currently only apply to typeclass proof search and the
+         :tacn:`typeclasses eauto` tactic.
+
+   .. cmd:: Hint Mode @qualid {+ {| + | ! | - } } {? : {+ @ident } }
+
+      Sets an optional mode of use for the identifier :n:`@qualid`. When
+      proof search has a goal that ends in an application of :n:`@qualid` to
+      arguments :n:`@arg ... @arg`, the mode tells if the hints associated with
+      :n:`@qualid` can be applied or not. A mode specification is a list of ``+``,
       ``!`` or ``-`` items that specify if an argument of the identifier is to be
       treated as an input (``+``), if its head only is an input (``!``) or an output
       (``-``) of the identifier. For a mode to match a list of arguments, input
       terms and input heads *must not* contain existential variables or be
-      existential variables respectively, while outputs can be any term. Multiple
-      modes can be declared for a single identifier, in that case only one mode
-      needs to match the arguments for the hints to be applied. The head of a term
+      existential variables respectively, while outputs can be any term.
+
+      The head of a term
       is understood here as the applicative head, or the match or projection
       scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is
       especially useful for typeclasses, when one does not want to support default
       instances and avoid ambiguity in general. Setting a parameter of a class as an
-      input forces proof-search to be driven by that index of the class, with ``!``
-      giving more flexibility by allowing existentials to still appear deeper in the
-      index but not at its head.
+      input forces proof search to be driven by that index of the class, with ``!``
+      allowing existentials to appear in the index but not at its head.
 
    .. note::
 
-      + One can use a :cmd:`Hint Extern` with no pattern to do
-        pattern matching on hypotheses using ``match goal with``
-        inside the tactic.
+      + Multiple modes can be declared for a single identifier.  In that
+        case only one mode needs to match the arguments for the hints to be applied.
 
       + If you want to add hints such as :cmd:`Hint Transparent`,
         :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass
         resolution, do not forget to put them in the
         ``typeclass_instances`` hint database.
 
+.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } }
+
+   :n:`{? using @ltac_expr }`
+     If specified, :n:`@ltac_expr` is applied to the generated subgoals, except for the
+     main subgoal.
+
+   :n:`{| -> | <- }`
+     Arrows specify the orientation; left to right (:n:`->`) or right to left (:n:`<-`).
+     If no arrow is given, the default orientation is left to right (:n:`->`).
+
+   Adds the terms :n:`{+ @one_term }` (their types must be
+   equalities) to the rewriting bases :n:`{*  @ident }`.
+   Note that the rewriting bases are distinct from the :tacn:`auto`
+   hint bases and that :tacn:`auto` does not take them into account.
+
+   .. cmd:: Print Rewrite HintDb @ident
+
+      This command displays all rewrite hints contained in :n:`@ident`.
+
+.. cmd:: Remove Hints {+ @qualid } {? : {+ @ident } }
+
+   Removes the hints associated with the :n:`{+ @qualid }` in databases
+   :n:`{+ @ident}`.  Note: hints created with :cmd:`Hint Extern` currently
+   can't be removed.  The best workaround for this is to make the hints
+   non global and carefully select which modules you import.
+
+.. cmd:: Print Hint {? {| * | @reference } }
+
+   :n:`*`
+     Display all declared hints.
+
+   :n:`@reference`
+     Display all hints associated with the head symbol :n:`@reference`.
+
+   Displays tactics from the hints list.  The default is to show hints that
+   apply to the conclusion of the current goal.  The other forms with :n:`*`
+   and :n:`@reference` can be used even if no proof is open.
+
+   Each hint has a cost that is a nonnegative
+   integer and an optional pattern. The hints with lower cost are tried first.
+
+.. cmd:: Print HintDb @ident
+
+   This command displays all hints from database :n:`@ident`.
+
 
 Hint databases defined in the Coq standard library
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--------------------------------------------------
 
 Several hint databases are defined in the Coq standard library. The
 actual content of a database is the collection of hints declared
@@ -555,76 +585,8 @@ At Coq startup, only the core database is nonempty and can be used.
 You are advised not to put your own hints in the core database, but
 use one or several databases specific to your development.
 
-.. _removehints:
-
-.. cmd:: Remove Hints {+ @term} : {+ @ident}
-
-   This command removes the hints associated to terms :n:`{+ @term}` in databases
-   :n:`{+ @ident}`.
-
-.. _printhint:
-
-.. cmd:: Print Hint
-
-   This command displays all hints that apply to the current goal. It
-   fails if no proof is being edited, while the two variants can be used
-   at every moment.
-
-**Variants:**
-
-
-.. cmd:: Print Hint @ident
-
-   This command displays only tactics associated with :n:`@ident` in the hints
-   list. This is independent of the goal being edited, so this command will not
-   fail if no goal is being edited.
-
-.. cmd:: Print Hint *
-
-   This command displays all declared hints.
-
-.. cmd:: Print HintDb @ident
-
-   This command displays all hints from database :n:`@ident`.
-
-.. _hintrewrite:
-
-.. cmd:: Hint Rewrite {+ @term} : {+ @ident}
-
-   This vernacular command adds the terms :n:`{+ @term}` (their types must be
-   equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation
-   (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto`
-   hint bases and that :tacn:`auto` does not take them into account.
-
-   This command is synchronous with the section mechanism (see :ref:`section-mechanism`):
-   when closing a section, all aliases created by ``Hint Rewrite`` in that
-   section are lost. Conversely, when loading a module, all ``Hint Rewrite``
-   declarations at the global level of that module are loaded.
-
-**Variants:**
-
-.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident}
-
-   This is strictly equivalent to the command above (we only make explicit the
-   orientation which otherwise defaults to ->).
-
-.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident}
-
-   Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in
-   the bases :n:`{+ @ident}`.
-
-.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } }
-
-   When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the
-   tactic ``tactic`` will be applied to the generated subgoals, the main subgoal
-   excluded.
-
-.. cmd:: Print Rewrite HintDb @ident
-
-   This command displays all rewrite hints contained in :n:`@ident`.
-
 Hint locality
-~~~~~~~~~~~~~
+-------------
 
 Hints provided by the ``Hint`` commands are erased when closing a section.
 Conversely, all hints of a module ``A`` that are not defined inside a
@@ -649,7 +611,6 @@ option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
 .. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" }
-   :name: Loose Hint Behavior
 
    This option accepts three values, which control the behavior of hints w.r.t.
    :cmd:`Import`:
@@ -668,22 +629,12 @@ non-imported hints.
 .. _tactics-implicit-automation:
 
 Setting implicit automation tactics
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-----------------------------------
 
-.. cmd:: Proof with @tactic
+.. cmd:: Proof with @ltac_expr {? using @section_var_expr }
 
-   This command may be used to start a proof. It defines a default tactic
-   to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``.
-   In this case the tactic command typed by the user is equivalent to
-   ``tactic``:sub:`1` ``;tactic``.
+   Starts a proof in which :token:`ltac_expr` is applied to the active goals
+   after each tactic that ends with `...` instead of the usual single period.
+   ":n:`@tactic...`" is equivalent to ":n:`@tactic; @ltac_expr.`".
 
    .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`.
-
-
-   .. cmdv:: Proof with @tactic using {+ @ident}
-
-      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
-
-   .. cmdv:: Proof using {+ @ident} with @tactic
-
-      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 9ec568c2c7..2de6b2a18c 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -295,21 +295,21 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 Performing computations
 ---------------------------
 
-.. insertprodn red_expr pattern_occ
+.. insertprodn red_expr pattern_occs
 
 .. prodn::
    red_expr ::= red
    | hnf
-   | simpl {? @delta_flag } {? @ref_or_pattern_occ }
+   | simpl {? @delta_flag } {? {| @reference_occs | @pattern_occs } }
    | cbv {? @strategy_flag }
    | cbn {? @strategy_flag }
    | lazy {? @strategy_flag }
    | compute {? @delta_flag }
-   | vm_compute {? @ref_or_pattern_occ }
-   | native_compute {? @ref_or_pattern_occ }
-   | unfold {+, @unfold_occ }
+   | vm_compute {? {| @reference_occs | @pattern_occs } }
+   | native_compute {? {| @reference_occs | @pattern_occs } }
+   | unfold {+, @reference_occs }
    | fold {+ @one_term }
-   | pattern {+, @pattern_occ }
+   | pattern {+, @pattern_occs }
    | @ident
    delta_flag ::= {? - } [ {+ @reference } ]
    strategy_flag ::= {+ @red_flag }
@@ -321,16 +321,8 @@ Performing computations
    | cofix
    | zeta
    | delta {? @delta_flag }
-   ref_or_pattern_occ ::= @reference {? at @occs_nums }
-   | @one_term {? at @occs_nums }
-   occs_nums ::= {+ @nat_or_var }
-   | - {+ @nat_or_var }
-   int_or_var ::= @integer
-   | @ident
-   nat_or_var ::= @natural
-   | @ident
-   unfold_occ ::= @reference {? at @occs_nums }
-   pattern_occ ::= @one_term {? at @occs_nums }
+   reference_occs ::= @reference {? at @occs_nums }
+   pattern_occs ::= @one_term {? at @occs_nums }
 
 This set of tactics implements different specialized usages of the
 tactic :tacn:`change`.
@@ -348,17 +340,6 @@ clauses) and are introduced by the keyword `in`. If no goal clause is
 provided, the default is to perform the conversion only in the
 conclusion.
 
-The syntax and description of the various goal clauses is the
-following:
-
-+ :n:`in {+ @ident} |-`  only in hypotheses :n:`{+ @ident}`
-+ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the
-  conclusion
-+ :n:`in * |-` in every hypothesis
-+ :n:`in *` (equivalent to in :n:`* |- *`) everywhere
-+ :n:`in (type of @ident) (value of @ident) ... |-` in type part of
-  :n:`@ident`, in the value part of :n:`@ident`, etc.
-
 For backward compatibility, the notation :n:`in {+ @ident}` performs
 the conversion in hypotheses :n:`{+ @ident}`.