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