Extruding the code for the Existential command from Proofview.

1 files changed, 20 insertions, 2 deletions

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