A "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0d50d521f3..4246cc9c7b 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 } =