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

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).

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
 ------------------------
 

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
 

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

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

doc/sphinx/conf.py

@@ -188,10 +188,8 @@ def setup(app):
     'conversion',
     'where',
     'oriented_rewriter',
-    'hintbases',
     'bindings_with_parameters',
-    'destruction_arg',
-    'clause_dft_concl'
+    'destruction_arg'
 ]]
 
 # -- Options for HTML output ----------------------------------------------

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

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.`

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

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.
 

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`

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::

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: