1 files changed, 51 insertions, 24 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305a..5c963d53 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
 
 exception FullyUnfocused
 
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Errors.error "This proof is focused, but cannot be unfocused this way"
+    CErrors.error "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      Errors.errorlabstrm "Focus" Pp.(
+      CErrors.errorlabstrm "Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
-  | FullyUnfocused -> Errors.error "The proof is not focused"
-  | _ -> raise Errors.Unhandled
+  | FullyUnfocused -> CErrors.error "The proof is not focused"
+  | _ -> raise CErrors.Unhandled
 end
 
 let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Errors.error "Some goals have not been solved."
-  | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
-  | HasGivenUpGoals -> Errors.error "Some goals have been given up."
-  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | UnfinishedProof -> CErrors.error "Some goals have not been solved."
+  | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
+  | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
+  | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+  | _ -> raise CErrors.Unhandled
 end
 
 let return p =
@@ -334,21 +334,30 @@ let compact p =
 (*** Tactics ***)
 
 let run_tactic env tac pr =
+  let open Proofview.Notations in
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
+  let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
+  let tac =
+    tac >>= fun () ->
+    Proofview.tclEVARMAP >>= fun sigma ->
+    (* Already solved goals are not to be counted as shelved. Nor are
+      they to be marked as unresolvable. *)
+    let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in
+    let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+    Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+    Proofview.tclUNIT retrieved
+  in
+  let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
     Proofview.apply env tac sp
   in
-  let sigma = Proofview.return tacticced_proofview in
-  (* Already solved goals are not to be counted as shelved. Nor are
-     they to be marked as unresolvable. *)
-  let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
-  let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let sigma = Proofview.return proofview in
+  let to_shelve = undef sigma to_shelve in
+  let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
   let proofview =
     List.fold_left
-      Proofview.Unsafe.mark_as_goal
-      tacticced_proofview
-      retrieved
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
   in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
@@ -387,9 +396,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
+          CErrors.error "incorrect existential variable index"
+        else if CList.length evl < n then
+          CErrors.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