Remove several calls to Evarutil.new_pure_evar.

1 files changed, 5 insertions, 10 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f553a290f9..f60151838a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -437,11 +437,6 @@ let clear_hyps2 env sigma ids sign t cl =
   with Evarutil.ClearDependencyError (id,err,inglobal) ->
     error_replacing_dependency env sigma id err inglobal
 
-let new_evar_from_context ?principal sign evd typ =
-  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
-  let (evd, evk) = Evarutil.new_pure_evar sign evd typ in
-  (evd, mkEvar (evk, instance))
-
 let internal_cut ?(check=true) replace id t =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -449,22 +444,22 @@ let internal_cut ?(check=true) replace id t =
     let concl = Proofview.Goal.concl gl in
     let sign = named_context_val env in
     let r = Retyping.relevance_of_type env sigma t in
-    let sign',t,concl,sigma =
+    let env',t,concl,sigma =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
         let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
-        sign',t,concl,sigma
+        Environ.reset_with_named_context sign' env,t,concl,sigma
       else
         (if check && mem_named_context_val id sign then
            user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
-         push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
+         push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in
     let nf_t = nf_betaiota env sigma t in
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
       (Refine.refine ~typecheck:false begin fun sigma ->
-        let (sigma, ev) = new_evar_from_context sign sigma nf_t in
-        let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in
+        let (sigma, ev) = Evarutil.new_evar env sigma nf_t in
+        let (sigma, ev') = Evarutil.new_evar ~principal:true env' sigma concl in
         let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
         (sigma, term)
       end)