Move connect_hint_clenv from Auto to Hints.

4 files changed, 30 insertions, 32 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..f485e7f02e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Termops
-open EConstr
 open Environ
 open Genredexpr
 open Tactics
@@ -69,33 +68,6 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv h gl =
-  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
-  (* [clenv] has been generated by a hint-making function, so the only relevant
-     data in its evarmap is the set of metas. The [evar_reset_evd] function
-     below just replaces the metas of sigma by those coming from the clenv. *)
-  let sigma = Tacmach.New.project gl in
-  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
-  (* Still, we need to update the universes *)
-  let clenv, c =
-    if h.hint_poly then
-      (* Refresh the instance of the hint *)
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let emap c = Vars.subst_univs_level_constr subst c in
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      (* Only metas are mentioning the old universes. *)
-      let clenv = {
-        templval = Evd.map_fl emap clenv.templval;
-        templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas emap evd;
-        env = Proofview.Goal.env gl;
-      } in
-      clenv, emap c
-    else
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
-  in clenv, c
-
 let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv h gl in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 903da143d2..bc2eee0e4c 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -12,7 +12,6 @@
 
 open Names
 open EConstr
-open Clenv
 open Pattern
 open Hints
 open Tactypes
@@ -23,9 +22,6 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
-val connect_hint_clenv
-  : hint -> Proofview.Goal.t -> clausenv * constr
-
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 386224824f..9fac66515a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1593,3 +1593,30 @@ struct
 
   let repr (h : t) = h.code.obj
 end
+
+let connect_hint_clenv h gl =
+  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
+  (* [clenv] has been generated by a hint-making function, so the only relevant
+     data in its evarmap is the set of metas. The [evar_reset_evd] function
+     below just replaces the metas of sigma by those coming from the clenv. *)
+  let sigma = Tacmach.New.project gl in
+  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+  (* Still, we need to update the universes *)
+  let clenv, c =
+    if h.hint_poly then
+      (* Refresh the instance of the hint *)
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+      let emap c = Vars.subst_univs_level_constr subst c in
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      (* Only metas are mentioning the old universes. *)
+      let clenv = {
+        templval = Evd.map_fl emap clenv.templval;
+        templtyp = Evd.map_fl emap clenv.templtyp;
+        evd = Evd.map_metas emap evd;
+        env = Proofview.Goal.env gl;
+      } in
+      clenv, emap c
+    else
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
+  in clenv, c
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8243716624..1508b81d1f 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -239,6 +239,9 @@ val wrap_hint_warning_fun : env -> evar_map ->
   (evar_map -> 'a * evar_map) -> 'a * evar_map
 (** Variant of the above for non-tactics *)
 
+val connect_hint_clenv
+  : hint -> Proofview.Goal.t -> clausenv * constr
+
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t