Extruding the code for the Existential command from Proofview.

5 files changed, 20 insertions, 35 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 059ae54c9..3192a6a29 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -59,14 +59,3 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
                  str (string_of_existential evk))
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
-
-(* vernac command Existential *)
-
-(* Main component of vernac command Existential *)
-let instantiate_pf_com evk com sigma =
-  let evi = Evd.find sigma evk in
-  let env = Evd.evar_filtered_env evi in
-  let rawc = Constrintern.intern_constr env com in
-  let ltac_vars = Pretyping.empty_lvar in
-  let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
-  sigma'
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 35a3e5d82..e3778e94c 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -13,8 +13,3 @@ open Pretyping
 
 val w_refine : evar * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
-
-val instantiate_pf_com :
-  Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map
-
-(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305aa..b604fde4e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -387,9 +387,27 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
 
+  (* Main component of vernac command Existential *)
   let instantiate_evar n com pr =
-    let sp = pr.proofview in
-    let proofview = Proofview.V82.instantiate_evar n com sp in
+    let tac =
+      Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+      let (evk, evi) =
+        let evl = Evarutil.non_instantiated sigma in
+        let evl = Evar.Map.bindings evl in
+        if (n <= 0) then
+          Errors.error "incorrect existential variable index"
+        else if CList.length evl < n then
+          Errors.error "not so many uninstantiated existential variables"
+        else
+          CList.nth evl (n-1)
+      in
+      let env = Evd.evar_filtered_env evi in
+      let rawc = Constrintern.intern_constr env com in
+      let ltac_vars = Pretyping.empty_lvar in
+      let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
+      Proofview.Unsafe.tclEVARS sigma
+    end in
+    let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a382e9873..b68fa042e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1272,20 +1272,6 @@ module V82 = struct
     in
     CList.flatten (CList.map evars_of_initial initial)
 
-  let instantiate_evar n com pv =
-    let (evk,_) =
-      let evl = Evarutil.non_instantiated pv.solution in
-      let evl = Evar.Map.bindings evl in
-      if (n <= 0) then
-	Errors.error "incorrect existential variable index"
-      else if CList.length evl < n then
-	  Errors.error "not so many uninstantiated existential variables"
-      else
-	CList.nth evl (n-1)
-    in
-    { pv with
-	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
-
   let of_tactic t gls =
     try
       let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7f95a053a..61014468b 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -577,9 +577,6 @@ module V82 : sig
   
   (* returns the existential variable used to start the proof *)
   val top_evars : entry -> Evd.evar list
-    
-  (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
 
   (* Caution: this function loses quite a bit of information. It
      should be avoided as much as possible.  It should work as