From b5e88d46530ba745f07a6d2664a0bba00f5f178a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 3 Sep 2013 18:18:43 +0000
Subject: Partly replacing list-based access functions in Evd. This is still
 unsatisfactory as some functions implicitly require some ordering on the
 evars, but this is already better.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proofview.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8a2c7617c6..843af1373b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -483,10 +483,11 @@ module V82 = struct
 
   (* Main function in the implementation of Grab Existential Variables.*)
   let grab pv =
+    let undef = Evd.undefined_map pv.solution in
     let goals =
       List.map begin fun (e,_) ->
 	Goal.build e
-      end (Evd.undefined_list pv.solution)
+      end (Evd.ExistentialMap.bindings undef)
     in
     { pv with comb = goals }
       
@@ -508,9 +509,10 @@ module V82 = struct
     List.flatten (List.map evars_of_initial initial)
 
   let instantiate_evar n com pv =
-    let (evk,_) = 
+    let (evk,_) =
       let evl = Evarutil.non_instantiated pv.solution in
-     if (n <= 0) then
+      let evl = Evd.ExistentialMap.bindings evl in
+      if (n <= 0) then
 	Errors.error "incorrect existential variable index"
       else if List.length evl < n then
 	  Errors.error "not so many uninstantiated existential variables"
-- 
cgit v1.2.3