From eabde14cce66553f9ba7b583507af51973ded850 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Feb 2020 10:29:01 +0100
Subject: Move the warning code out of the parser.

---
 tactics/hints.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'tactics')

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) =
-- 
cgit v1.2.3


From db4cbfef3226cd999b3554b9b8160bc331f45c05 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Feb 2020 10:34:29 +0100
Subject: Deprecate the OCaml API to declare term Hints.

---
 tactics/class_tactics.ml | 3 ++-
 tactics/hints.mli        | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 28feeecb86..02186f6a98 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.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
-- 
cgit v1.2.3