Adapt the documentation after deprecation of term hints.

Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.

1 files changed, 22 insertions, 22 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2fa4f1fa42..aee62f1b27 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3761,18 +3761,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
@@ -3780,32 +3780,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
@@ -3813,12 +3813,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