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

Reviewed-by: Zimmi48
Ack-by: JasonGross

22 files changed, 718 insertions, 825 deletions

diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst
index f37fbfe52b..e63241e46c 100644
--- a/doc/changelog/04-tactics/13381-bfs_eauto.rst
+++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst
@@ -1,6 +1,6 @@
 - **Deprecated:**
-  Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``.
-  Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``.
-  (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.)
+  Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`.
+  Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`.
+  (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.)
   (`#13381 <https://github.com/coq/coq/pull/13381>`_,
   by Jim Fehrle).
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
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 24fa71059c..249c7794be 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -551,7 +551,7 @@ Flags, options and attributes
   ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
   Théo Zimmermann).
 - **Added:**
-  The :cmd:`Hint` commands now accept the :attr:`export` locality as
+  The :ref:`Hint <creating_hints>` commands now accept the :attr:`export` locality as
   an attribute, allowing to make import-scoped hints
   (`#11812 <https://github.com/coq/coq/pull/11812>`_,
   by Pierre-Marie Pédrot).
@@ -3170,7 +3170,7 @@ Vernacular Commands
   `Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
 - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
   globally the opacity flag of variables and constants in hint databases,
-  overwriting the opacity set of the hint database.
+  overriding the opacity setting of the hint database.
 - Added generic syntax for "attributes", as in:
   `#[local] Lemma foo : bar.`
 - Added the `Numeral Notation` command for registering decimal numeral
@@ -4045,7 +4045,7 @@ constraints can now be left floating around and be seen by the user
 thanks to a new option. The Keyed Unification mode has been improved by
 Matthieu Sozeau.
 
-The typeclass resolution engine and associated proof-search tactic have
+The typeclass resolution engine and associated proof search tactic have
 been reimplemented on top of the proof-engine monad, providing better
 integration in tactics, and new options have been introduced to control
 it, by Matthieu Sozeau with help from Théo Zimmermann.
@@ -5140,7 +5140,7 @@ Program
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
 - Documented the Hint Cut command that allows control of the
-  proof-search during typeclass resolution (see reference manual).
+  proof search during typeclass resolution (see reference manual).
 
 API
 
@@ -5776,7 +5776,7 @@ Libraries
   comes first. By default, the power function now takes two BigN.
 
 - Creation of Vector, an independent library for lists indexed by their length.
-  Vectors' names overwrite lists' one so you should not "Import" the library.
+  Vectors' names override lists' one so you should not "Import" the library.
   All old names changed: function names follow the ocaml ones and, for example,
   Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
   Vector.VectorNotations.
@@ -6830,7 +6830,7 @@ Tactics
 - Tactic "remember" now supports an "in" clause to remember only selected
   occurrences of a term.
 
-- Tactic "pose proof" supports name overwriting in case of specialization of an
+- Tactic "pose proof" supports name overriding in case of specialization of an
   hypothesis.
 
 - Semi-decision tactic "jp" for first-order intuitionistic logic moved to user
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index af5d1e3a00..246568d3c1 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -188,10 +188,8 @@ nitpick_ignore = [ ('token', token) for token in [
     'conversion',
     'where',
     'oriented_rewriter',
-    'hintbases',
     'bindings_with_parameters',
-    'destruction_arg',
-    'clause_dft_concl'
+    'destruction_arg'
 ]]
 
 # -- Options for HTML output ----------------------------------------------
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 251b5e4955..9fda2ab1fa 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -8,14 +8,13 @@ Inductive types
 
 .. cmd:: Inductive @inductive_definition {* with @inductive_definition }
 
-   .. insertprodn inductive_definition cumul_ident_decl
+   .. insertprodn inductive_definition constructor
 
    .. prodn::
-      inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      inductive_definition ::= {? > } @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
       | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
-      cumul_ident_decl ::= @ident {? @cumul_univ_decl }
 
    This command defines one or more
    inductive types and its constructors.  Coq generates destructors
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 54252689e1..6d96e15202 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -155,7 +155,8 @@ are now available through the dot notation.
   #. Interactive modules and module types can be nested.
   #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`.
      Sections can be defined inside of interactive modules and module types.
-  #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive
+  #. Hints and notations (the :ref:`Hint <creating_hints>` and :cmd:`Notation`
+     commands) can also appear inside interactive
      modules and module types. Note that with module definitions like:
 
      :n:`Module @ident__1 : @module_type := @ident__2.`
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index df50dbafe3..75389bb259 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -69,7 +69,8 @@ Sections create local contexts which can be shared across multiple definitions.
        :undocumented:
 
 .. note::
-   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
+   Most commands, such as the :ref:`Hint <creating_hints>` commands,
+   :cmd:`Notation` and option management commands that
    appear inside a section are canceled when the section is closed.
 
 .. cmd:: Let @ident_decl @def_body
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2fc3c9f748..87a367fc93 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1637,9 +1637,10 @@ Testing boolean expressions: guard
 .. tacn:: guard @int_or_var @comparison @int_or_var
    :name: guard
 
-   .. insertprodn comparison comparison
+   .. insertprodn int_or_var comparison
 
    .. prodn::
+      int_or_var ::= {| @integer | @ident }
       comparison ::= =
       | <
       | <=
@@ -1761,7 +1762,7 @@ Defining |Ltac| symbols
          "Ltac intros := idtac" seems like it redefines/hides an
          existing tactic, but in fact it creates a tactic which can
          only be called by its qualified name.  This is true in
-         general of tactic notations.  The only way to overwrite most
+         general of tactic notations.  The only way to override most
          primitive tactics, and any user-defined tactic notation, is
          with another tactic notation.
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index a46f4fb894..375129c02d 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1475,7 +1475,7 @@ Other nonterminals that have syntactic classes are listed here.
 
       * - :n:`clause`
         - :token:`ltac2_clause`
-        - :token:`clause_dft_concl`
+        - :token:`occurrences`
 
       * - :n:`occurrences`
         - :token:`q_occurrences`
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4f01559cad..8f5c045929 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -466,52 +466,82 @@ Examples:
 
 .. _occurrencessets:
 
-Occurrence sets and occurrence clauses
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-An occurrence clause is a modifier to some tactics that obeys the
-following syntax:
-
-  .. prodn::
-     occurrence_clause ::= in @goal_occurrences
-     goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } }
-     | * |- {? * {? @at_occurrences } }
-     | *
-     at_occurrences ::= at @occurrences
-     occurrences ::= {? - } {* @natural }
-
-The role of an occurrence clause is to select a set of occurrences of a term
-in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate
-that occurrences have to be selected in the hypotheses named :token:`ident`.
-If no numbers are given for hypothesis :token:`ident`, then all the
-occurrences of :token:`term` in the hypothesis are selected. If numbers are
-given, they refer to occurrences of :token:`term` when the term is printed
-using the :flag:`Printing All` flag, counting from left to right. In particular,
-occurrences of :token:`term` in implicit arguments
-(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are
-counted.
-
-If a minus sign is given between ``at`` and the list of occurrences, it
-negates the condition so that the clause denotes all the occurrences
-except the ones explicitly mentioned after the minus sign.
-
-As an exception to the left-to-right order, the occurrences in
-the return subexpression of a match are considered *before* the
-occurrences in the matched term.
-
-In the second case, the ``*`` on the left of ``|-`` means that all occurrences
-of term are selected in every hypothesis.
-
-In the first and second case, if ``*`` is mentioned on the right of ``|-``, the
-occurrences of the conclusion of the goal have to be selected. If some numbers
-are given, then only the occurrences denoted by these numbers are selected. If
-no numbers are given, all occurrences of :token:`term` in the goal are selected.
-
-Finally, the last notation is an abbreviation for ``* |- *``. Note also
-that ``|-`` is optional in the first case when no ``*`` is given.
-
-Here are some tactics that understand occurrence clauses: :tacn:`set`,
-:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`.
+Occurrence clauses
+~~~~~~~~~~~~~~~~~~
+
+An :gdef:`occurrence` is a subterm of a goal or hypothesis that
+matches a pattern provided by a tactic.  Occurrence clauses
+select a subset of the ocurrences in a goal and/or in
+one or more of its hypotheses.
+
+   .. insertprodn occurrences concl_occs
+
+   .. prodn::
+      occurrences ::= at @occs_nums
+      | in @goal_occurrences
+      occs_nums ::= {? - } {+ @nat_or_var }
+      nat_or_var ::= {| @natural | @ident }
+      goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } }
+      | * %|- {? @concl_occs }
+      | %|- {? @concl_occs }
+      | {? @concl_occs }
+      hyp_occs ::= @hypident {? at @occs_nums }
+      hypident ::= @ident
+      | ( type of @ident )
+      | ( value of @ident )
+      concl_occs ::= * {? at @occs_nums }
+
+   :n:`@occurrences`
+     The first form of :token:`occurrences` selects occurrences in
+     the conclusion of the goal.  The second form can select occurrences
+     in the goal conclusion and in one or more hypotheses.
+
+   :n:`{? - } {+ @nat_or_var }`
+     Selects the specified occurrences within a single goal or hypothesis.
+     Occurrences are numbered from left to right starting with 1 when the
+     goal is printed with the :flag:`Printing All` flag.  (In particular, occurrences
+     in :ref:`implicit arguments <ImplicitArguments>` and
+     :ref:`coercions <Coercions>` are counted but not shown by default.)
+
+     Specifying `-` includes all occurrences *except* the ones listed.
+
+   :n:`{*, @hyp_occs } {? %|- {? @concl_occs } }`
+     Selects occurrences in the specified hypotheses and the
+     specified occurrences in the conclusion.
+
+   :n:`* %|- {? @concl_occs }`
+     Selects all occurrences in all hypotheses and the
+     specified occurrences in the conclusion.
+
+   :n:`%|- {? @concl_occs }`
+     Selects the specified occurrences in the conclusion.
+
+   :n:`@goal_occurrences ::= {? @concl_occs }`
+     Selects all occurrences in all hypotheses and in the specified occurrences
+     in the conclusion.
+
+   :n:`@hypident {? at @occs_nums }`
+     Omiting :token:`occs_nums` selects all occurrences within the hypothesis.
+
+   :n:`@hypident ::= @ident`
+     Selects the hypothesis named :token:`ident`.
+
+   :n:`( type of @ident )`
+     Selects the type part of the named hypothesis (e.g. `: nat`).
+
+   :n:`( value of @ident )`
+     Selects the value part of the named hypothesis (e.g. `:= 1`).
+
+   :n:`@concl_occs ::= * {? at @occs_nums }`
+     Selects occurrences in the conclusion.  '*' by itself selects all occurrences.
+     :n:`@occs_nums` selects the specified occurrences.
+
+   Use `in *` to select all occurrences in all hypotheses and the conclusion,
+   which is equivalent to `in * |- *`.  Use `* |-` to select all occurrences
+   in all hypotheses.
+
+Tactics that use occurrence clauses include :tacn:`set`,
+:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`.
 
 
 .. seealso::
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 86d1d25745..e7db9cfaca 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1136,7 +1136,7 @@ Controlling the locality of commands
    Some commands support an :attr:`export` attribute.  The effect of
    the attribute is to make the effect of the command available when
    the module containing it is imported.  It is supported in
-   particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset`
+   particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset`
    commands.
 
 .. _controlling-typing-flags:
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}`.
 
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 6c507e1d57..ba5876ff76 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -181,9 +181,6 @@ as a separate production.  (Doesn't work recursively; splicing for both
 
 `OPTINREF` - applies the local `OPTINREF` edit to every nonterminal
 
-`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into
-new non-terminals
-
 ### Local edits
 
 `DELETE <production>` - removes the specified production from the grammar
@@ -201,6 +198,9 @@ that appear in the specified production:
   The current version handles a single USE_NT or ADD_OPT per EDIT.  These symbols
   may appear in the middle of the production given in the EDIT.
 
+`APPENDALL <symbols>` - inserts <symbols> at the end of every production in
+<edited_nt>.
+
 `INSERTALL <symbols>` - inserts <symbols> at the beginning of every production in
 <edited_nt>.
 
@@ -212,10 +212,12 @@ that appear in the specified production:
 | WITH <newprod>
 ```
 
+`COPYALL <destination>` - creates a new nonterminal `<destination>` and copies
+all the productions in the nonterminal to `<destination>`.
+
 `MOVETO <destination> <production>` - moves the production to `<destination>` and,
  if needed, creates a new production <edited_nt> -> \<destination>.
 
-
 `MOVEALLBUT <destination>` - moves all the productions in the nonterminal to `<destination>`
 *except* for the productions following the `MOVEALLBUT` production in the edit script
 (terminated only by the closing `]`).
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4080eaae08..8efda825de 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -19,8 +19,22 @@ lglob: [
 ]
 
 hint: [
+| REPLACE "Resolve" "->" LIST1 global OPT natural
+| WITH "Resolve" [ "->" | "<-" ] LIST1 global OPT natural
+| DELETE "Resolve" "<-" LIST1 global OPT natural
+| REPLACE "Variables" "Transparent"
+| WITH [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ]
+| DELETE "Variables" "Opaque"
+| DELETE "Constants" "Transparent"
+| DELETE "Constants" "Opaque"
+| REPLACE "Transparent" LIST1 global
+| WITH [ "Transparent" | "Opaque" ] LIST1 global
+| DELETE "Opaque" LIST1 global
+
 | REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
 | WITH "Extern" natural OPT constr_pattern "=>" tactic
+| INSERTALL "Hint"
+| APPENDALL opt_hintbases
 ]
 
 (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *)
@@ -149,6 +163,7 @@ DELETE: [
 | ensure_fixannot
 | test_array_opening
 | test_array_closing
+| test_variance_ident
 
   (* SSR *)
 | ssr_null_entry
@@ -267,7 +282,7 @@ binder_constr: [
 | REPLACE "if" term200 "is" ssr_dthen ssr_else
 | WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR
 | DELETE "if" term200 "isn't" ssr_dthen ssr_else
-| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR  (* todo: restore for SSR *)
+| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR  (* todo: restore as "MOVETO term_if" for SSR *)
 | MOVETO term_fix "let" "fix" fix_decl "in" term200
 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
@@ -597,6 +612,11 @@ univ_decl: [
 | WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
+cumul_univ_decl: [
+| REPLACE "@{" LIST0 variance_identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| WITH "@{" LIST0 variance_identref    OPT "+"   OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
 of_type: [
 | DELETENT
 ]
@@ -905,12 +925,13 @@ where: [
 ]
 
 simple_tactic: [
-| DELETE "intros"
-| REPLACE "intros" ne_intropatterns
-| WITH "intros" intropatterns
-| DELETE "eintros"
-| REPLACE "eintros" ne_intropatterns
-| WITH "eintros" intropatterns
+| REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "eauto" OPT nat_or_var auto_using hintbases
+| REPLACE "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "debug" "eauto" OPT nat_or_var auto_using hintbases
+| REPLACE "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "info_eauto" OPT nat_or_var auto_using hintbases
+
 | DELETE "autorewrite" "with" LIST1 preident clause
 | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic
 | DELETE "autorewrite" "*" "with" LIST1 preident clause
@@ -966,6 +987,12 @@ simple_tactic: [
 | DELETE "intro" "after" hyp
 | DELETE "intro" "before" hyp
 | "intro" OPT ident OPT where
+| DELETE "intros"
+| REPLACE "intros" ne_intropatterns
+| WITH "intros" intropatterns
+| DELETE "eintros"
+| REPLACE "eintros" ne_intropatterns
+| WITH "eintros" intropatterns
 | DELETE "move" hyp "at" "top"
 | DELETE "move" hyp "at" "bottom"
 | DELETE "move" hyp "after" hyp
@@ -1139,6 +1166,10 @@ printable: [
 | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
 | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
 | DELETE "Term" smart_global OPT univ_name_list  (* readded in commands *)
+| REPLACE "Hint"
+| WITH "Hint" OPT [ "*" | smart_global ]
+| DELETE "Hint" smart_global
+| DELETE "Hint" "*"
 
 | INSERTALL "Print"
 ]
@@ -1163,6 +1194,8 @@ scheme_kind: [
 command: [
 | REPLACE "Print" printable
 | WITH printable
+| REPLACE "Hint" hint opt_hintbases
+| WITH hint
 | "SubClass" ident_decl def_body
 | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
 | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
@@ -1242,6 +1275,9 @@ command: [
 | REPLACE "Preterm" "of" ident
 | WITH "Preterm" OPT ( "of" ident )
 | DELETE "Preterm"
+| REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic
+| WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ]
+| DELETE "Proof" "using" section_var_expr
 
 (* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Remove" IDENT IDENT LIST1 table_value
@@ -1441,8 +1477,8 @@ type_cstr: [
 ]
 
 inductive_definition: [
-| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
-| WITH    opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ]    opt_constructors_or_fields decl_notations
+| REPLACE opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+| WITH    opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" type ]    opt_constructors_or_fields decl_notations
 ]
 
 (* note that constructor -> identref constructor_type *)
@@ -1578,9 +1614,12 @@ simple_reserv: [
 
 in_clause: [
 | DELETE in_clause'
-| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ
-| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ )
-| DELETE LIST0 hypident_occ SEP ","
+| REPLACE LIST1 hypident_occ SEP "," "|-" concl_occ
+| WITH LIST1 hypident_occ SEP "," OPT ( "|-" concl_occ )
+| DELETE LIST1 hypident_occ SEP ","
+| REPLACE "*" occs
+| WITH concl_occ
+(* todo: perhaps concl_occ should be "*" | "at" occs_nums *)
 ]
 
 ltac2_in_clause: [
@@ -1791,6 +1830,7 @@ tactic_notation_tactics: [
 | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
 | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
 | "intuition" OPT ltac_expr5  (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *)
+| "now" ltac_expr5
 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
 | "psatz" constr OPT nat_or_var
 | "ring" OPT ( "[" LIST1 constr "]" )
@@ -1942,6 +1982,18 @@ tac2rec_fields: [
 | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
 ]
 
+int_or_var: [
+| REPLACE integer
+| WITH [ integer | identref ]
+| DELETE identref
+]
+
+nat_or_var: [
+| REPLACE natural
+| WITH [ natural | identref ]
+| DELETE identref
+]
+
 ltac2_occs_nums: [
 | DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
 | REPLACE "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
@@ -2387,6 +2439,33 @@ attribute: [
 | DELETE "using" OPT attr_value
 ]
 
+hypident: [
+(* todo: restore for SSR *)
+| DELETE "(" "type" "of" ident ")"      (* SSR plugin *)
+| DELETE "(" "value" "of" ident ")"      (* SSR plugin *)
+]
+
+ref_or_pattern_occ: [
+| DELETE smart_global OPT occs
+| DELETE constr OPT occs
+| unfold_occ
+| pattern_occ
+]
+
+clause_dft_concl: [
+(* omit an OPT since clause_dft_concl is always OPT *)
+| REPLACE OPT occs
+| WITH occs
+]
+
+occs_nums: [
+| EDIT ADD_OPT "-" LIST1 nat_or_var
+]
+
+variance_identref: [
+| EDIT ADD_OPT variance identref
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2526,6 +2605,7 @@ SPLICE: [
 | eliminator  (* todo: splice or not? *)
 | quoted_attributes  (* todo: splice or not? *)
 | printable
+| hint
 | only_parsing
 | record_fields
 | constructor_type
@@ -2606,9 +2686,18 @@ SPLICE: [
 | syn_level
 | firstorder_rhs
 | firstorder_using
+| hints_path_atom
+| ref_or_pattern_occ
+| cumul_ident_decl
+| variance
+| variance_identref
 ] (* end SPLICE *)
 
 RENAME: [
+| occurrences rewrite_occs
+]
+
+RENAME: [
 | tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
@@ -2652,6 +2741,13 @@ RENAME: [
 | ssrclauses ssr_in
 | ssrcpat ssrblockpat
 | constr_pattern one_pattern
+| hints_path hints_regexp
+| clause_dft_concl occurrences
+| in_clause goal_occurrences
+| unfold_occ reference_occs
+| pattern_occ pattern_occs
+| hypident_occ hyp_occs
+| concl_occ concl_occs
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 92a745c863..dd7990368e 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -527,28 +527,28 @@ let rec edit_SELF nt cur_level next_level right_assoc inner prod =
   prod
 
 
-let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
+let autoloaded_mlgs = [ (* productions from other mlgs are marked with TAGs *)
  "parsing/g_constr.mlg";
  "parsing/g_prim.mlg";
- "vernac/g_vernac.mlg";
- "vernac/g_proofs.mlg";
- "toplevel/g_toplevel.mlg";
- "plugins/ltac/extraargs.mlg";
- "plugins/ltac/g_obligations.mlg";
+ "plugins/btauto/g_btauto.mlg";
+ "plugins/cc/g_congruence.mlg";
+ "plugins/firstorder/g_ground.mlg";
  "plugins/ltac/coretactics.mlg";
+ "plugins/ltac/extraargs.mlg";
  "plugins/ltac/extratactics.mlg";
- "plugins/ltac/profile_ltac_tactics.mlg";
  "plugins/ltac/g_auto.mlg";
  "plugins/ltac/g_class.mlg";
- "plugins/ltac/g_rewrite.mlg";
  "plugins/ltac/g_eqdecide.mlg";
- "plugins/ltac/g_tactic.mlg";
  "plugins/ltac/g_ltac.mlg";
- "plugins/btauto/g_btauto.mlg";
+ "plugins/ltac/g_obligations.mlg";
+ "plugins/ltac/g_rewrite.mlg";
+ "plugins/ltac/g_tactic.mlg";
+ "plugins/ltac/profile_ltac_tactics.mlg";
  "plugins/rtauto/g_rtauto.mlg";
- "plugins/cc/g_congruence.mlg";
- "plugins/firstorder/g_ground.mlg";
  "plugins/syntax/g_number_string.mlg";
+ "toplevel/g_toplevel.mlg";
+ "vernac/g_proofs.mlg";
+ "vernac/g_vernac.mlg";
 ]
 
 
@@ -1020,7 +1020,7 @@ let rec gen_nt_name sym =
   good_name name
 
 (* create a new nt for LIST* or OPT with the specified name *)
-let rec maybe_add_nt g insert_after name sym queue =
+let maybe_add_nt g insert_after name sym queue =
   let empty = [Snterm "empty"] in
   let maybe_unwrap ?(multi=false) sym =
     match sym with
@@ -1094,65 +1094,6 @@ let rec maybe_add_nt g insert_after name sym queue =
   end;
   new_nt
 
-(* expand LIST*, OPT and add "empty" *)
-(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *)
-and expand_rule g edited_nt queue =
-  let rule = NTMap.find edited_nt !g.map in
-  let insert_after = ref edited_nt in
-  let rec expand rule =
-    let rec aux syms res =
-      match syms with
-      | [] -> res
-      | sym0 :: tl ->
-        let new_sym = match sym0 with
-          | Sterm _
-          | Snterm _ ->
-            sym0
-          | Slist1 sym
-          | Slist1sep (sym, _)
-          | Slist0 sym
-          | Slist0sep (sym, _)
-          | Sopt sym ->
-            let name = gen_nt_name sym in
-            if name <> "" then begin
-              let new_nt = maybe_add_nt g insert_after name sym0 queue in
-              Snterm new_nt
-            end else sym0
-          | Sparen slist -> Sparen (expand slist)
-          | Sprod slistlist ->
-            let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in
-            let name = gen_nt_name sym0 in
-            if name <> "" then begin
-              let new_nt = maybe_add_nt g insert_after name
-                  (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) ))
-                  else sym0) queue
-              in
-              Snterm new_nt
-            end else
-              Sprod (List.map expand slistlist)
-          | Sedit _
-          | Sedit2 _ ->
-            sym0 (* these constructors not used here *)
-        in
-        aux tl (new_sym :: res)
-    in
-    List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else []))
-  in
-  let rule' = List.map expand rule in
-  g_update_prods g edited_nt rule'
-
-let expand_lists g =
-  (* todo: use Queue.of_seq w OCaml 4.07+ *)
-  let queue = Queue.create () in
-  List.iter (fun nt -> Queue.add nt queue) !g.order;
-  try
-    while true do
-      let nt = Queue.pop queue in
-      expand_rule g nt queue
-    done
-  with
-  | Queue.Empty -> ()
-
 let apply_merge g edit_map =
   List.iter (fun b ->
       let (from_nt, to_nt) = b in
@@ -1213,10 +1154,6 @@ let edit_all_prods g op eprods =
           global_repl g [(Snterm nt)] [(Sopt (Snterm nt))]
         end)
       !g.order; true
-  | "EXPAND" ->
-    if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then
-      error "'EXPAND:' expects a single empty production\n";
-    expand_lists g; true
   | _ -> false
 
 let edit_single_prod g edit0 prods nt =
@@ -1281,6 +1218,11 @@ let apply_edit_file g edits =
             with Not_found -> prods in
             let prods' = moveto nt dest_nt oprod prods in
             aux tl prods' add_nt
+          | [Snterm "COPYALL"; Snterm dest_nt] :: tl ->
+            if NTMap.mem dest_nt !g.map then
+              error "COPYALL target nonterminal `%s` already exists\n" dest_nt;
+            g_maybe_add g dest_nt prods;
+            aux tl prods add_nt
           | [Snterm "MOVEALLBUT"; Snterm dest_nt] :: tl ->
             List.iter (fun tlprod ->
                 if not (List.mem tlprod prods) then
@@ -1300,6 +1242,8 @@ let apply_edit_file g edits =
             aux tl (remove_prod [] prods nt) add_nt
           | (Snterm "INSERTALL" :: syms) :: tl ->
             aux tl (List.map (fun p -> syms @ p) prods) add_nt
+          | (Snterm "APPENDALL" :: syms) :: tl ->
+            aux tl (List.map (fun p -> p @ syms) prods) add_nt
           | (Snterm "PRINT" :: _) :: tl ->
             pr_prods nt prods;
             aux tl prods add_nt
@@ -1395,56 +1339,6 @@ let nt_subset_in_orig_order g nts =
   let subset = StringSet.of_list nts in
   List.filter (fun nt -> StringSet.mem nt subset) !g.order
 
-let print_chunk out g seen fmt title starts ends =
-  fprintf out "\n\n%s:\n%s\n" title header;
-  List.iter (fun start ->
-      let nts = (nt_closure g start ends) in
-      print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen;
-      seen := StringSet.union !seen (StringSet.of_list nts))
-    starts
-
-let print_chunks g out fmt () =
-  let seen = ref StringSet.empty in
-  print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"];
-  print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"];
-  print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"];
-  print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"];
-  print_chunk out g seen fmt "simple_tactic" ["simple_tactic"]
-    ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"];
-
-  (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*)
-  print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"];
-  print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"];
-  print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"];
-  print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"];
-  print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"];
-  print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] [];
-
-
-  print_chunk out g seen fmt "command" ["command"] [];
-  print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];
-  print_chunk out g seen fmt "vernac_control" ["vernac_control"] []
-
-  (*
-    let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in
-    seen := StringSet.union !seen (StringSet.of_list ssr_tops);
-
-    print_chunk out g seen fmt "ssrindex" ["ssrindex"] [];
-    print_chunk out g seen fmt "command" ["command"] [];
-    print_chunk out g seen fmt "binder_constr" ["binder_constr"] [];
-    (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*)
-    print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] [];
-    (*print_chunk out g seen fmt "hloc" ["hloc"] [];*)
-    (*print_chunk out g seen fmt "hypident" ["hypident"] [];*)
-    print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] [];
-    print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] [];
-    fprintf out "\n\nRemainder:\n";
-    print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty;
-  *)
-
-
-    (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*)
-    (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*)
 let index_of str list =
   let rec index_of_r str list index =
     match list with
@@ -1478,89 +1372,6 @@ let get_range g start end_ =
 
 let get_rangeset g start end_ = StringSet.of_list (get_range g start end_)
 
-let print_dominated g =
-  let info nt rangeset exclude =
-    let reachable = StringSet.of_list (nt_closure g nt exclude) in
-    let unreachable = StringSet.of_list (nt_closure g (List.hd start_symbols) (nt::exclude)) in
-    let dominated = StringSet.diff reachable unreachable in
-    Printf.printf "For %s, 'attribute' is: reachable = %b, unreachable = %b, dominated = %b\n" nt
-        (StringSet.mem "attribute" reachable)
-        (StringSet.mem "attribute" unreachable)
-        (StringSet.mem "attribute" dominated);
-    Printf.printf "  rangeset = %b excluded = %b\n"
-        (StringSet.mem "attribute" rangeset)
-        (List.mem "attribute" exclude);
-    reachable, dominated
-  in
-  let pr3 nt rangeset reachable dominated =
-    let missing = StringSet.diff dominated rangeset in
-    if not (StringSet.is_empty missing) then begin
-      Printf.printf "\nMissing in range for '%s':\n" nt;
-      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) missing
-    end;
-
-    let unneeded = StringSet.diff rangeset reachable in
-    if not (StringSet.is_empty unneeded) then begin
-      Printf.printf "\nUnneeded in range for '%s':\n" nt;
-      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) unneeded
-    end;
-  in
-  let pr2 nt rangeset exclude =
-    let reachable, dominated = info nt rangeset exclude in
-    pr3 nt rangeset reachable dominated
-  in
-  let pr nt end_ = pr2 nt (get_rangeset g nt end_) [] in
-
-  let ssr_ltac = ["ssr_first_else"; "ssrmmod"; "ssrdotac"; "ssrortacarg";
-      "ssrparentacarg"] in
-  let ssr_tac = ["ssrintrosarg"; "ssrhintarg"; "ssrtclarg"; "ssrseqarg"; "ssrmovearg";
-      "ssrrpat"; "ssrclauses"; "ssrcasearg"; "ssrarg"; "ssrapplyarg"; "ssrexactarg";
-      "ssrcongrarg"; "ssrterm"; "ssrrwargs"; "ssrunlockargs"; "ssrfixfwd"; "ssrcofixfwd";
-      "ssrfwdid"; "ssrposefwd"; "ssrsetfwd"; "ssrdgens"; "ssrhavefwdwbinders"; "ssrhpats_nobs";
-      "ssrhavefwd"; "ssrsufffwd"; "ssrwlogfwd"; "ssrhint"; "ssrclear"; "ssr_idcomma";
-      "ssrrwarg"; "ssrintros_ne"; "ssrhint3arg" ] @ ssr_ltac in
-  let ssr_cmd = ["ssr_modlocs"; "ssr_search_arg"; "ssrhintref"; "ssrhintref_list";
-      "ssrviewpos"; "ssrviewposspc"] in
-  let ltac = ["ltac_expr"; "ltac_expr0"; "ltac_expr1"; "ltac_expr2"; "ltac_expr3"] in
-  let term = ["term"; "term0"; "term1"; "term10"; "term100"; "term9";
-      "pattern"; "pattern0"; "pattern1"; "pattern10"] in
-
-  pr "term" "constr";
-
-  let ltac_rangeset = List.fold_left StringSet.union StringSet.empty
-                            [(get_rangeset g "ltac_expr" "tactic_atom");
-                            (get_rangeset g "toplevel_selector" "range_selector");
-                            (get_rangeset g "ltac_match_term" "match_pattern");
-                            (get_rangeset g "ltac_match_goal" "match_pattern_opt")] in
-  pr2 "ltac_expr" ltac_rangeset ("simple_tactic" :: ssr_tac);
-
-  let dec_vern_rangeset = get_rangeset g "decorated_vernac" "opt_coercion" in
-  let dev_vern_excl =
-      ["gallina_ext"; "command"; "tactic_mode"; "syntax"; "command_entry"] @ term @ ltac @ ssr_tac in
-  pr2 "decorated_vernac" dec_vern_rangeset dev_vern_excl;
-
-  let simp_tac_range = get_rangeset g "simple_tactic" "hypident_occ_list_comma" in
-  let simp_tac_excl = ltac @ ssr_tac in
-  pr2 "simple_tactic" simp_tac_range simp_tac_excl;
-
-  let cmd_range = get_rangeset g "command" "int_or_id_list_opt" in
-  let cmd_excl = ssr_tac @ ssr_cmd in
-  pr2 "command" cmd_range cmd_excl;
-
-  let syn_range = get_rangeset g "syntax" "constr_as_binder_kind" in
-  let syn_excl = ssr_tac @ ssr_cmd in
-  pr2 "syntax" syn_range syn_excl;
-
-  let gext_range = get_rangeset g "gallina_ext" "Structure_opt" in
-  let gext_excl = ssr_tac @ ssr_cmd in
-  pr2 "gallina_ext" gext_range gext_excl;
-
-  let qry_range = get_rangeset g "query_command" "searchabout_query_list" in
-  let qry_excl = ssr_tac @ ssr_cmd in
-  pr2 "query_command" qry_range qry_excl
-
-  (* todo: tactic_mode *)
-
 let check_range_consistency g start end_ =
   let defined_list = get_range g start end_ in
   let defined = StringSet.of_list defined_list in
@@ -1913,13 +1724,8 @@ let process_rst g file args seen tac_prods cmd_prods =
     end
   in
 
-(*  let skip_files = ["doc/sphinx/proof-engine/ltac.rst"; "doc/sphinx/proof-engine/ltac2.rst";*)
-(*    "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*)
-(*  in*)
-
   let cmd_exclude_files = [
     "doc/sphinx/proof-engine/ssreflect-proof-language.rst";
-    "doc/sphinx/proofs/automatic-tactics/auto.rst";
     "doc/sphinx/proofs/writing-proofs/rewriting.rst";
     "doc/sphinx/proofs/writing-proofs/proof-mode.rst";
     "doc/sphinx/proof-engine/tactics.rst";
@@ -2101,7 +1907,6 @@ let process_grammar args =
       close_out out;
       finish_with_file (dir "orderedGrammar") args;
 (*      check_singletons g*)
-(*      print_dominated g*)
 
       let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
       let args = { args with no_update = false } in (* always update rsts in place for now *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index d01f66c6d7..cf90eea5a1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -342,6 +342,21 @@ closed_binder: [
 | [ "of" | "&" ] term99      (* SSR plugin *)
 ]
 
+one_open_binder: [
+| name
+| name ":" lconstr
+| one_closed_binder
+]
+
+one_closed_binder: [
+| "(" name ":" lconstr ")"
+| "{" name "}"
+| "{" name ":" lconstr "}"
+| "[" name "]"
+| "[" name ":" lconstr "]"
+| "'" pattern0
+]
+
 typeclass_constraint: [
 | "!" term200
 | "{" name "}" ":" [ "!" | ] term200
@@ -875,10 +890,29 @@ univ_decl: [
 | "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
 ]
 
+variance: [
+| "+"
+| "="
+| "*"
+]
+
+variance_identref: [
+| identref
+| test_variance_ident variance identref
+]
+
+cumul_univ_decl: [
+| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+]
+
 ident_decl: [
 | identref OPT univ_decl
 ]
 
+cumul_ident_decl: [
+| identref OPT cumul_univ_decl
+]
+
 finite_token: [
 | "Inductive"
 | "CoInductive"
@@ -918,7 +952,7 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
 ]
 
 constructors_or_record: [
@@ -1914,8 +1948,9 @@ in_clause: [
 | in_clause'
 | "*" occs
 | "*" "|-" concl_occ
-| LIST0 hypident_occ SEP "," "|-" concl_occ
-| LIST0 hypident_occ SEP ","
+| "|-" concl_occ
+| LIST1 hypident_occ SEP "," "|-" concl_occ
+| LIST1 hypident_occ SEP ","
 ]
 
 test_lpar_id_colon: [
@@ -2493,7 +2528,7 @@ in_hyp_list: [
 ]
 
 in_hyp_as: [
-| "in" id_or_meta as_ipat
+| "in" LIST1 [ id_or_meta as_ipat ] SEP ","
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index f62dd8f731..7c709baa48 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -436,7 +436,7 @@ univ_decl: [
 ]
 
 cumul_univ_decl: [
-| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| "@{" LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
 univ_constraint: [
@@ -512,6 +512,21 @@ binder: [
 | "'" pattern0
 ]
 
+one_open_binder: [
+| name
+| name ":" term
+| one_closed_binder
+]
+
+one_closed_binder: [
+| "(" name ":" term ")"
+| "{" name "}"
+| "{" name ":" term "}"
+| "[" name "]"
+| "[" name ":" term "]"
+| "'" pattern0
+]
+
 implicit_binders: [
 | "{" LIST1 name OPT ( ":" type ) "}"
 | "[" LIST1 name OPT ( ":" type ) "]"
@@ -614,16 +629,16 @@ reduce: [
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" OPT delta_flag OPT ref_or_pattern_occ
+| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ]
 | "cbv" OPT strategy_flag
 | "cbn" OPT strategy_flag
 | "lazy" OPT strategy_flag
 | "compute" OPT delta_flag
-| "vm_compute" OPT ref_or_pattern_occ
-| "native_compute" OPT ref_or_pattern_occ
-| "unfold" LIST1 unfold_occ SEP ","
+| "vm_compute" OPT [ reference_occs | pattern_occs ]
+| "native_compute" OPT [ reference_occs | pattern_occs ]
+| "unfold" LIST1 reference_occs SEP ","
 | "fold" LIST1 one_term
-| "pattern" LIST1 pattern_occ SEP ","
+| "pattern" LIST1 pattern_occs SEP ","
 | ident
 ]
 
@@ -646,31 +661,11 @@ red_flag: [
 | "delta" OPT delta_flag
 ]
 
-ref_or_pattern_occ: [
+reference_occs: [
 | reference OPT ( "at" occs_nums )
-| one_term OPT ( "at" occs_nums )
-]
-
-occs_nums: [
-| LIST1 nat_or_var
-| "-" LIST1 nat_or_var
-]
-
-int_or_var: [
-| integer
-| ident
 ]
 
-nat_or_var: [
-| natural
-| ident
-]
-
-unfold_occ: [
-| reference OPT ( "at" occs_nums )
-]
-
-pattern_occ: [
+pattern_occs: [
 | one_term OPT ( "at" occs_nums )
 ]
 
@@ -705,7 +700,7 @@ field_def: [
 ]
 
 inductive_definition: [
-| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+| OPT ">" ident OPT cumul_univ_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
 constructors_or_record: [
@@ -717,10 +712,6 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
-cumul_ident_decl: [
-| ident OPT cumul_univ_decl
-]
-
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]
@@ -901,9 +892,7 @@ command: [
 | "Print" "Typing" "Flags"
 | "Print" "Tables"
 | "Print" "Options"
-| "Print" "Hint"
-| "Print" "Hint" reference
-| "Print" "Hint" "*"
+| "Print" "Hint" OPT [ "*" | reference ]
 | "Print" "HintDb" ident
 | "Print" "Scopes"
 | "Print" "Scope" scope_name
@@ -958,7 +947,6 @@ command: [
 | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
 | "Proof"
-| "Proof" "using" section_var_expr
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
@@ -983,7 +971,6 @@ command: [
 | "Guarded"
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
-| "Hint" hint OPT ( ":" LIST1 ident )
 | "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
@@ -1030,7 +1017,7 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
+| "Hint" "Cut" "[" hints_regexp "]" OPT ( ":" LIST1 ident )
 | "Prenex" "Implicits" LIST1 qualid      (* SSR plugin *)
 | "Print" "Hint" "View" OPT ssrviewpos      (* SSR plugin *)
 | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) )      (* SSR plugin *)
@@ -1039,7 +1026,7 @@ command: [
 | "Typeclasses" "Opaque" LIST1 qualid
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
 | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ]
-| "Proof" "using" section_var_expr "with" ltac_expr
+| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
@@ -1142,6 +1129,15 @@ command: [
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
 | "Print" "Ltac2" qualid      (* Ltac2 plugin *)
+| "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident )
+| "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident )
+| "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident )
+| "Hint" [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ] OPT ( ":" LIST1 ident )
+| "Hint" [ "Transparent" | "Opaque" ] LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Mode" qualid LIST1 [ "+" | "!" | "-" ] OPT ( ":" LIST1 ident )
+| "Hint" "Unfold" LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Constructors" LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Extern" natural OPT one_pattern "=>" ltac_expr OPT ( ":" LIST1 ident )
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" natural sentence
@@ -1205,23 +1201,6 @@ univ_name_list: [
 | "@{" LIST0 name "}"
 ]
 
-hint: [
-| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
-| "Resolve" "->" LIST1 qualid OPT natural
-| "Resolve" "<-" LIST1 qualid OPT natural
-| "Immediate" LIST1 [ qualid | one_term ]
-| "Variables" "Transparent"
-| "Variables" "Opaque"
-| "Constants" "Transparent"
-| "Constants" "Opaque"
-| "Transparent" LIST1 qualid
-| "Opaque" LIST1 qualid
-| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
-| "Unfold" LIST1 qualid
-| "Constructors" LIST1 qualid
-| "Extern" natural OPT one_pattern "=>" ltac_expr
-]
-
 tacdef_body: [
 | qualid LIST0 name [ ":=" | "::=" ] ltac_expr
 ]
@@ -1275,28 +1254,37 @@ constr_with_bindings_arg: [
 | OPT ">" one_term OPT ( "with" bindings )      (* SSR plugin *)
 ]
 
-clause_dft_concl: [
-| "in" in_clause
-| OPT ( "at" occs_nums )
+occurrences: [
+| "at" occs_nums
+| "in" goal_occurrences
 ]
 
-in_clause: [
-| "*" OPT ( "at" occs_nums )
-| "*" "|-" OPT concl_occ
-| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
+occs_nums: [
+| OPT "-" LIST1 nat_or_var
 ]
 
-hypident_occ: [
+nat_or_var: [
+| [ natural | ident ]
+]
+
+goal_occurrences: [
+| LIST1 hyp_occs SEP "," OPT ( "|-" OPT concl_occs )
+| "*" "|-" OPT concl_occs
+| "|-" OPT concl_occs
+| OPT concl_occs
+]
+
+hyp_occs: [
 | hypident OPT ( "at" occs_nums )
 ]
 
 hypident: [
 | ident
-| "(" "type" "of" ident ")"      (* SSR plugin *)
-| "(" "value" "of" ident ")"      (* SSR plugin *)
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
 ]
 
-concl_occ: [
+concl_occs: [
 | "*" OPT ( "at" occs_nums )
 ]
 
@@ -1545,15 +1533,15 @@ number_string_via: [
 | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
 ]
 
-hints_path: [
-| "(" hints_path ")"
-| hints_path "*"
-| "emp"
-| "eps"
-| hints_path "|" hints_path
+hints_regexp: [
 | LIST1 qualid
 | "_"
-| hints_path hints_path
+| hints_regexp "|" hints_regexp
+| hints_regexp hints_regexp
+| hints_regexp "*"
+| "emp"
+| "eps"
+| "(" hints_regexp ")"
 ]
 
 class: [
@@ -1630,7 +1618,7 @@ simple_tactic: [
 | "constructor" OPT nat_or_var OPT ( "with" bindings )
 | "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) )
 | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern )
-| "symmetry" OPT ( "in" in_clause )
+| "symmetry" OPT ( "in" goal_occurrences )
 | "split" OPT ( "with" bindings )
 | "esplit" OPT ( "with" bindings )
 | "exists" OPT ( LIST1 bindings SEP "," )
@@ -1648,8 +1636,8 @@ simple_tactic: [
 | "clear" "-" LIST1 ident
 | "clearbody" LIST1 ident
 | "generalize" "dependent" one_term
-| "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 )
-| "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl
+| "replace" one_term "with" one_term OPT occurrences OPT ( "by" ltac_expr3 )
+| "replace" OPT [ "->" | "<-" ] one_term OPT occurrences
 | "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
 | OPT ( [ natural | "[" ident "]" ] ":" ) "{"
 | bullet
@@ -1701,9 +1689,9 @@ simple_tactic: [
 | "decompose" "record" one_term
 | "absurd" one_term
 | "contradiction" OPT ( one_term OPT ( "with" bindings ) )
-| "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr )
-| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) )
-| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 )
+| "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 )
 | "refine" one_term
 | "simple" "refine" one_term
 | "notypeclasses" "refine" one_term
@@ -1764,13 +1752,13 @@ simple_tactic: [
 | "auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "info_auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases
-| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases
-| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
-| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "debug" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
+| "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
-| "autounfold" OPT hintbases OPT clause_dft_concl
+| "autounfold" OPT hintbases OPT occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
 | "convert_concl_no_check" one_term
@@ -1784,8 +1772,8 @@ simple_tactic: [
 | "rewrite_strat" rewstrategy OPT ( "in" ident )
 | "rewrite_db" ident OPT ( "in" ident )
 | "substitute" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings )
-| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" occurrences ) OPT ( "in" ident )
-| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" occurrences
+| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" rewrite_occs ) OPT ( "in" ident )
+| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" rewrite_occs
 | "setoid_symmetry" OPT ( "in" ident )
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
@@ -1808,10 +1796,10 @@ simple_tactic: [
 | "pose" one_term OPT as_name
 | "epose" bindings_with_parameters
 | "epose" one_term OPT as_name
-| "set" bindings_with_parameters OPT clause_dft_concl
-| "set" one_term OPT as_name OPT clause_dft_concl
-| "eset" bindings_with_parameters OPT clause_dft_concl
-| "eset" one_term OPT as_name OPT clause_dft_concl
+| "set" bindings_with_parameters OPT occurrences
+| "set" one_term OPT as_name OPT occurrences
+| "eset" bindings_with_parameters OPT occurrences
+| "eset" one_term OPT as_name OPT occurrences
 | "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
 | "eremember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
 | "assert" "(" ident ":=" term ")"
@@ -1829,32 +1817,32 @@ simple_tactic: [
 | "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
 | "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
 | "generalize" one_term OPT ( LIST1 one_term )
-| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT as_name ]
+| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occs OPT as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
 | "edestruct" induction_clause_list
-| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
-| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
+| "rewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
+| "erewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
 | "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ]
 | "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
-| "red" OPT clause_dft_concl
-| "hnf" OPT clause_dft_concl
-| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
-| "cbv" OPT strategy_flag OPT clause_dft_concl
-| "cbn" OPT strategy_flag OPT clause_dft_concl
-| "lazy" OPT strategy_flag OPT clause_dft_concl
-| "compute" OPT delta_flag OPT clause_dft_concl
-| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
-| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
-| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl
-| "fold" LIST1 one_term OPT clause_dft_concl
-| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl
-| "change" conversion OPT clause_dft_concl
-| "change_no_check" conversion OPT clause_dft_concl
+| "red" OPT occurrences
+| "hnf" OPT occurrences
+| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] OPT occurrences
+| "cbv" OPT strategy_flag OPT occurrences
+| "cbn" OPT strategy_flag OPT occurrences
+| "lazy" OPT strategy_flag OPT occurrences
+| "compute" OPT delta_flag OPT occurrences
+| "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
+| "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
+| "unfold" LIST1 reference_occs SEP "," OPT occurrences
+| "fold" LIST1 one_term OPT occurrences
+| "pattern" LIST1 pattern_occs SEP "," OPT occurrences
+| "change" conversion OPT occurrences
+| "change_no_check" conversion OPT occurrences
 | "btauto"
 | "rtauto"
 | "congruence" OPT natural OPT ( "with" LIST1 one_term )
@@ -1946,6 +1934,7 @@ simple_tactic: [
 | "field_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident )
 | "intuition" OPT ltac_expr
+| "now" ltac_expr
 | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term )
 | "psatz" one_term OPT nat_or_var
 | "ring" OPT ( "[" LIST1 one_term "]" )
@@ -1998,19 +1987,24 @@ induction_clause_list: [
 | LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause
 ]
 
-induction_clause: [
-| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
-]
-
 opt_clause: [
-| "in" in_clause
+| "in" goal_occurrences
 | "at" occs_nums
 ]
 
+induction_clause: [
+| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
+]
+
 auto_using: [
 | "using" LIST1 one_term SEP ","
 ]
 
+hintbases: [
+| "with" "*"
+| "with" LIST1 ident
+]
+
 or_and_intropattern: [
 | "[" intropattern_or_list_or "]"
 | "(" LIST0 simple_intropattern SEP "," ")"
@@ -2055,6 +2049,10 @@ bindings: [
 | LIST1 one_term
 ]
 
+int_or_var: [
+| [ integer | ident ]
+]
+
 comparison: [
 | "="
 | "<"
@@ -2063,11 +2061,6 @@ comparison: [
 | ">="
 ]
 
-hintbases: [
-| "with" "*"
-| "with" LIST1 ident
-]
-
 bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
@@ -2436,11 +2429,11 @@ tac2mode: [
 ]
 
 clause_dft_all: [
-| "in" in_clause
+| "in" goal_occurrences
 ]
 
 in_hyp_as: [
-| "in" ident OPT as_ipat
+| "in" LIST1 [ ident OPT as_ipat ] SEP ","
 ]
 
 simple_binder: [
@@ -2470,7 +2463,7 @@ func_scheme_def: [
 | ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
 
-occurrences: [
+rewrite_occs: [
 | LIST1 integer
 | ident
 ]
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 236d35b68e..c489d82d0b 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -236,8 +236,6 @@ Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
 
-(** A HintDb for crelations. *)
-
 Ltac solve_crelation :=
   match goal with
   | [ |- ?R ?x ?x ] => reflexivity
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 54ee06343a..353496dfba 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -235,8 +235,6 @@ Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
 
-(** A HintDb for relations. *)
-
 Ltac solve_relation :=
   match goal with
   | [ |- ?R ?x ?x ] => reflexivity