From 8e30bdf78eb5feb274b16fb1db1c7350e771ee99 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 7 Feb 2012 16:51:46 +0000
Subject: 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
---
 proofs/proofview.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'proofs/proofview.ml')

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 } = 
-- 
cgit v1.2.3