From 511a3eae36d3b57afbbb37b586ef71adf094f8ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Oct 2020 18:41:39 +0200
Subject: Encapsulate the last use of IsConstr in the Hints API.

---
 tactics/hints.ml  | 8 ++++++++
 tactics/hints.mli | 5 +++--
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0170487b2e..b8bd459616 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1347,6 +1347,14 @@ let add_hints ~locality dbnames h =
   | HintsExternEntry (info, tacexp) ->
       add_externs info tacexp ~local ~superglobal dbnames
 
+let hint_constr env sigma ~poly c =
+  let c, diff = prepare_hint true env sigma c in
+  let diff, uctx =
+    if poly then Some diff, Univ.ContextSet.empty
+    else None, diff
+  in
+  IsConstr (c, diff), uctx
+
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
     match EConstr.kind sigma lem with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1bbb506761..e74519f12a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -199,8 +199,9 @@ val current_pure_db : unit -> hint_db list
 
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
-val prepare_hint : bool (* Check no remaining evars *) ->
-  env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
+val hint_constr :
+  env -> evar_map -> poly:bool -> evar_map * constr -> hint_term * Univ.ContextSet.t
+  [@ocaml.deprecated "Declare a hint constant instead"]
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
-- 
cgit v1.2.3