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

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

3 files changed, 13 insertions, 3 deletions

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