From aaafa92638be941a8750b1d88f42be69b807e550 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 May 2011 17:57:57 +0000
Subject: A better procedure for checking presence of undefined evars.

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

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index aa00cee829..dd65a90495 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -467,9 +467,7 @@ module V82 = struct
 }
 
   let has_unresolved_evar pv =
-    let evd = pv.solution in
-    (* arnaud: essayer une procédure moins coûteuse *)
-    not ((Evarutil.non_instantiated evd) = [])
+    Evd.has_undefined pv.solution
 
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
-- 
cgit v1.2.3