Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve description of Instance command

Reviewed-by: Zimmi48

4 files changed, 33 insertions, 26 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index cdd31fcb86..56d90b33d8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -336,20 +336,23 @@ Summary of the commands
 
 .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } }
 
-   .. insertprodn hint_info hint_info
+   .. insertprodn hint_info one_pattern
 
    .. prodn::
-      hint_info ::= %| {? @natural } {? @one_term }
+      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
    the class.
 
-   Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
-   specifies the hint priority, where 0 is the highest priority as for
+   Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
+   may be used to specify the hint priority, where 0 is the highest priority as for
    :tacn:`auto` hints. If the priority is not specified, the default is the number
-   of non-dependent binders of the instance.
+   of non-dependent binders of the instance.  If :token:`one_pattern` is given, terms
+   matching that pattern will trigger use of the instance.  Otherwise,
+   use is triggered based on the conclusion of the type.
 
    This command supports the :attr:`global` attribute that can be
    used on instances declared in a section so that their
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7baf193266..86d1d25745 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -133,7 +133,7 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
    .. prodn::
       search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key }
-      | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term
+      | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern
       | is : @logical_kind
 
    Searched objects can be filtered by patterns, by the constants they
@@ -141,9 +141,9 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
    names.
    The location of the pattern or constant within a term
 
-   :n:`@one_term`
+   :n:`@one_pattern`
       Search for objects whose type contains a subterm matching the
-      pattern :n:`@one_term`.  Holes of the pattern are indicated by
+      pattern :n:`@one_pattern`.  Holes of the pattern are indicated by
       `_` or :n:`?@ident`.  If the same :n:`?@ident` occurs more than
       once in the pattern, all occurrences in the subterm must be
       identical.  See :ref:`this example <search-pattern>`.
@@ -312,7 +312,7 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
          Search is:Instance [ Reflexive | Symmetric ].
 
-.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } }
 
    .. deprecated:: 8.12
 
@@ -320,8 +320,8 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
    Displays the name and type of all hypotheses of the
    selected goal (if any) and theorems of the current context that have the
-   form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term`
-   matches a subterm of `C` in head position.  For example, a :n:`@one_term` of `f _ b`
+   form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern`
+   matches a subterm of `C` in head position.  For example, a :n:`@one_pattern` of `f _ b`
    matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`.
 
    See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
@@ -337,12 +337,12 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
          SearchHead le.
          SearchHead (@eq bool).
 
-.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } }
 
    Displays the name and type of all hypotheses of the
    selected goal (if any) and theorems of the current context
    ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern
-   :n:`@one_term`.
+   :n:`@one_pattern`.
 
    See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
 
@@ -362,11 +362,11 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
          SearchPattern (?X1 + _ = _ + ?X1).
 
-.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } }
 
    Displays the name and type of all hypotheses of the
    selected goal (if any) and theorems of the current context that have the form
-   :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term`
+   :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern`
    matches either `LHS` or `RHS`.
 
    See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 116fcaa87b..4c1956d172 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2481,7 +2481,6 @@ SPLICE: [
 | binders
 | casted_constr
 | check_module_types
-| constr_pattern
 | decl_sep
 | function_fix_definition (* loses funind annotation *)
 | glob
@@ -2655,6 +2654,7 @@ RENAME: [
 | ssrfwd ssrdefbody
 | ssrclauses ssr_in
 | ssrcpat ssrblockpat
+| constr_pattern one_pattern
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 6b12d90d5d..26474d950a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -728,7 +728,11 @@ sort_family: [
 ]
 
 hint_info: [
-| "|" OPT natural OPT one_term
+| "|" OPT natural OPT one_pattern
+]
+
+one_pattern: [
+| one_term
 ]
 
 module_binder: [
@@ -1015,7 +1019,7 @@ command: [
 | "Prenex" "Implicits" LIST1 qualid      (* SSR plugin *)
 | "Print" "Hint" "View" OPT ssrviewpos      (* SSR plugin *)
 | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) )      (* SSR plugin *)
-| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) )      (* SSR plugin *)
+| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) )      (* SSR plugin *)
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
@@ -1111,9 +1115,9 @@ command: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
@@ -1171,7 +1175,7 @@ search_query: [
 
 search_item: [
 | OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
-| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern
 | "is" ":" logical_kind
 ]
 
@@ -1200,7 +1204,7 @@ hint: [
 | "Mode" qualid LIST1 [ "+" | "!" | "-" ]
 | "Unfold" LIST1 qualid
 | "Constructors" LIST1 qualid
-| "Extern" natural OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_pattern "=>" ltac_expr
 ]
 
 tacdef_body: [
@@ -2408,9 +2412,9 @@ tac2mode: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 ]