From aba870c6b58b18bc1bd4711c379863a87bbf6d33 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 19:54:19 +0200
Subject: Remove Evarutil.new_evar_from_context from the API.

---
 tactics/tactics.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4804822c99..7269b5c02d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -436,6 +436,10 @@ 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
+  Evarutil.new_evar_instance sign evd typ instance
+
 let internal_cut ?(check=true) replace id t =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -457,8 +461,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)
-- 
cgit v1.2.3


From 834c64015b608b8152e160d37e6f07a3106ff26b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 20:02:42 +0200
Subject: Remove Evarutil.new_evar_instance from the API.

---
 tactics/tactics.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7269b5c02d..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
 
@@ -438,7 +439,8 @@ let clear_hyps2 env sigma ids sign t cl =
 
 let new_evar_from_context ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
-  Evarutil.new_evar_instance sign evd typ instance
+  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 ->
-- 
cgit v1.2.3