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.

---
 vernac/classes.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac')

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