From 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 Jun 2018 17:02:34 +0200
Subject: Deprecating the declaration of arbitrary terms as hints.

We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
---
 vernac/g_proofs.mlg | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 03dfc576a1..596b04f7e3 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -43,6 +43,13 @@ let warn_deprecated_unfocus =
   CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated"
          (fun () -> Pp.strbrk "The Unfocus command is deprecated")
 
+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"
+         )
+
 }
 
 (* Proof commands *)
@@ -107,7 +114,9 @@ GRAMMAR EXTEND Gram
       ] ];
   reference_or_constr:
    [ [ r = global -> { HintsReference r }
-     | c = constr -> { HintsConstr c } ] ]
+     | c = constr ->
+      { warn_deprecated_hint_constr ~loc ();
+        HintsConstr c } ] ]
   ;
   hint:
     [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
-- 
cgit v1.2.3


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.

---
 vernac/g_proofs.mlg | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 596b04f7e3..03dfc576a1 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -43,13 +43,6 @@ let warn_deprecated_unfocus =
   CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated"
          (fun () -> Pp.strbrk "The Unfocus command is deprecated")
 
-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"
-         )
-
 }
 
 (* Proof commands *)
@@ -114,9 +107,7 @@ GRAMMAR EXTEND Gram
       ] ];
   reference_or_constr:
    [ [ r = global -> { HintsReference r }
-     | c = constr ->
-      { warn_deprecated_hint_constr ~loc ();
-        HintsConstr c } ] ]
+     | c = constr -> { HintsConstr c } ] ]
   ;
   hint:
     [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
-- 
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.

---
 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