Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.

Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes

2 files changed, 27 insertions, 22 deletions

diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst
new file mode 100644
index 0000000000..d2af6a4ca7
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst
@@ -0,0 +1,5 @@
+- **Deprecated:**
+  Deprecated the declaration of arbitrary terms as hints. Global
+  references are now mandatory.
+  (`#7791 <https://github.com/coq/coq/pull/7791>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 206342fef1..2bfd810ea1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3774,18 +3774,18 @@ automatically created.
       Local is useless since hints do not survive anyway to the closure of
       sections.
 
-   .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident
+   .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident
       :name: Hint Resolve
 
-      This command adds :n:`simple apply @term` to the hint list with the head
-      symbol of the type of :n:`@term`. The cost of that hint is the number of
-      subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
+      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:`@num` if specified. The
       associated :n:`@pattern` is inferred from the conclusion of the type of
-      :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
-      of :n:`@term` does not start with a product the tactic added in the hint list
-      is :n:`exact @term`. In case this type can however be reduced to a type
-      starting with a product, the tactic :n:`simple apply @term` is also stored in
-      the hints list. If the inferred type of :n:`@term` contains a dependent
+      :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
       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
@@ -3793,32 +3793,32 @@ automatically created.
       typical example of a hint that is used only by :tacn:`eauto` is a transitivity
       lemma.
 
-      .. exn:: @term cannot be used as a hint
+      .. exn:: @qualid cannot be used as a hint
 
-         The head symbol of the type of :n:`@term` is a bound variable
+         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 {+ @term} : @ident
+   .. cmdv:: Hint Resolve {+ @qualid} : @ident
 
-      Adds each :n:`Hint Resolve @term`.
+      Adds each :n:`Hint Resolve @qualid`.
 
-   .. cmdv:: Hint Resolve -> @term : @ident
+   .. cmdv:: Hint Resolve -> @qualid : @ident
 
       Adds the left-to-right implication of an equivalence as a hint (informally
-      the hint will be used as :n:`apply <- @term`, although as mentioned
+      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 <- @term
+   .. cmdv:: Hint Resolve <- @qualid
 
       Adds the right-to-left implication of an equivalence  as a hint.
 
-   .. cmdv:: Hint Immediate @term : @ident
+   .. cmdv:: Hint Immediate @qualid : @ident
       :name: Hint Immediate
 
-      This command adds :n:`simple apply @term; trivial` to the hint list associated
+      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 @term` are
+      tactic will fail if all the subgoals generated by :n:`simple apply @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
@@ -3826,12 +3826,12 @@ automatically created.
       never generates subgoals) is always 1, so that it is not used by :tacn:`trivial`
       itself.
 
-   .. exn:: @term cannot be used as a hint
+   .. exn:: @qualid cannot be used as a hint
       :undocumented:
 
-   .. cmdv:: Hint Immediate {+ @term} : @ident
+   .. cmdv:: Hint Immediate {+ @qualid} : @ident
 
-      Adds each :n:`Hint Immediate @term`.
+      Adds each :n:`Hint Immediate @qualid`.
 
    .. cmdv:: Hint Constructors @qualid : @ident
       :name: Hint Constructors