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

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

6 files changed, 43 insertions, 26 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
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e49f5abb8c..e3f2f18b44 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -528,9 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
           let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in
             (List.map_append
              (fun (path,info,c) ->
+              let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
               make_resolves env sigma ~name:(PathHints path)
                   (true,false,not !Flags.quiet) info ~poly:false
-                 (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
+                 h)
                hints)
         else []
       in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 86aa046586..731792e34e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r =
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
 
+let warn_deprecated_hint_constr =
+  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+         (fun () ->
+           Pp.strbrk
+             "Declaring arbitrary terms as hints is deprecated; declare a global reference instead"
+         )
+
 let interp_hints ~poly =
   fun h ->
   let env = Global.env () in
@@ -1349,7 +1356,9 @@ let interp_hints ~poly =
     | HintsReference c ->
       let gr = global_with_alias c in
         (PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c -> (PathAny, poly, f poly c)
+    | HintsConstr c ->
+      let () = warn_deprecated_hint_constr () in
+      (PathAny, poly, f poly c)
   in
   let fp = Constrintern.intern_constr_pattern env sigma in
   let fres (info, b, r) =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9c9f0b7708..7bb17489bf 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -181,7 +181,7 @@ type hnf = bool
 
 type hint_term =
   | IsGlobRef of GlobRef.t
-  | IsConstr of constr * Univ.ContextSet.t
+  | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"]
 
 type hints_entry =
   | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b92c9e9b71..16b9e07fb2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -60,7 +60,9 @@ let add_instance check inst =
   let local = is_local_for_hint inst in
   add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local
     inst.is_info poly;
-  List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path
+  List.iter (fun (path, pri, c) ->
+    let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in
+    add_instance_hint h path
                 local pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)