Split the uses of connect_hint_clenv into two different functions.

The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.

5 files changed, 52 insertions, 59 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1ba35e9113..0931c3e61e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -15,7 +15,6 @@ open Termops
 open Environ
 open Genredexpr
 open Tactics
-open Clenv
 open Locus
 open Proofview.Notations
 open Hints
@@ -78,10 +77,10 @@ let unify_resolve_gen = function
 
 let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv h gl in
-    Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-    (exact_check c)
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = Hints.fresh_hint env sigma h in
+    Proofview.Unsafe.tclEVARS sigma <*> exact_check c
   end
 
 (* Util *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 64d62a89b0..c4ef32974c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,18 +144,11 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
 }
 
 let e_give_exact flags h =
-  let { hint_term = c; hint_uctx = ctx } = h in
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
   let sigma = project gl in
-  let c, sigma =
-    if h.hint_poly then
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let evd = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-      let c = Vars.subst_univs_level_constr subst c in
-      c, evd
-    else c, sigma
-  in
+  let sigma, c = Hints.fresh_hint env sigma h in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
   Proofview.Unsafe.tclEVARS sigma <*>
   Clenv.unify ~flags t1 <*> exact_no_check c
@@ -179,28 +172,21 @@ let unify_resolve ~with_evars flags h diff = match diff with
 let unify_resolve_refine flags h diff =
   let len = match diff with None -> None | Some (diff, _) -> Some diff in
   Proofview.Goal.enter begin fun gls ->
-  let { hint_term = c; hint_type = t; hint_uctx = ctx } = h in
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
   Refine.refine ~typecheck:false begin fun sigma ->
-      let sigma, term, ty =
-        if h.hint_poly then
-          let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-          let map c = Vars.subst_univs_level_constr subst c in
-          let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-          sigma, map c, map t
-        else
-          let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-          sigma, c, t
-      in
-      let sigma', cl = Clenv.make_evar_clause env sigma ?len ty in
-      let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
-      let sigma' =
-        Evarconv.(unify_leq_delay
-                    ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
-                              env sigma' cl.cl_concl concl)
-      in (sigma', term) end
+    let sigma, term = Hints.fresh_hint env sigma h in
+    let ty = Retyping.get_type_of env sigma term in
+    let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
+    let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
+    let sigma =
+      Evarconv.(unify_leq_delay
+                  ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
+                            env sigma cl.cl_concl concl)
+    in
+    (sigma, term)
+    end
   end
 
 let unify_resolve_refine flags h diff =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 1bdf36b56c..9a554b117e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -19,7 +19,6 @@ open Tacticals
 open Tacmach
 open Evd
 open Tactics
-open Clenv
 open Auto
 open Genredexpr
 open Tactypes
@@ -84,10 +83,10 @@ let hintmap_of sigma secvars concl =
 
 let e_exact flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv h gl in
-    Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-    (e_give_exact c)
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = Hints.fresh_hint env sigma h in
+    Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c
   end
 
 let rec e_trivial_fail_db db_list local_db =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 683691d5c4..e029e4628d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1595,34 +1595,44 @@ struct
 end
 
 let connect_hint_clenv h gl =
-  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
+  let { 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
+  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
+  else
+    let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+
+let fresh_hint env sigma h =
+  let { hint_term = c; hint_uctx = ctx } = h in
+  if h.hint_poly then
+    (* Refresh the instance of the hint *)
+    let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+    let c = Vars.subst_univs_level_constr subst c in
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
+  else
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
 
 let hint_res_pf ?with_evars ?with_classes ?flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv, _ = connect_hint_clenv h gl in
+    let clenv = connect_hint_clenv h gl in
     Clenv.res_pf ?with_evars ?with_classes ?flags clenv
   end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index d8b6458c27..f0fed75828 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -239,8 +239,7 @@ 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
+val fresh_hint : env -> evar_map -> hint -> evar_map * constr
 
 val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
   ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic