Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 11 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0d50d521..4246cc9c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -475,6 +475,17 @@ module V82 = struct
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
+  (* Main function in the implementation of Grab Existential Variables.*)
+  let grab pv =
+    let goals =
+      List.map begin fun (e,_) ->
+	Goal.build e
+      end (Evd.undefined_list pv.solution)
+    in
+    { pv with comb = goals }
+      
+    
+
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
   let goals { comb = comb ; solution = solution } =