Merge PR #12645: Cleanup Evarutil API

Reviewed-by: ejgallego
Reviewed-by: herbelin

1 files changed, 11 insertions, 5 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4804822c99..f553a290f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -120,8 +120,8 @@ let unsafe_intro env decl b =
     let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
-    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
-    (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
+    let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in
+    (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) (mkEvar (ev, ninst)))
   end
 
 let introduction id =
@@ -340,7 +340,8 @@ let rename_hyp repl =
       let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~typecheck:false begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
+        let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in
+        sigma, mkEvar (ev, instance)
       end
     end
 
@@ -436,6 +437,11 @@ 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
@@ -457,8 +463,8 @@ let internal_cut ?(check=true) replace id t =
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
       (Refine.refine ~typecheck:false begin fun sigma ->
-        let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
-        let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
+        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 term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
         (sigma, term)
       end)