From e2d04d6e3370b043351ec7f7648b4c54f9505d80 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 29 Apr 2005 18:34:01 +0000
Subject: Protection against saving a proof with still non-instantiated evars
 (cf bug #901) (continued!)

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

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 804d009b14..ca5d53587d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -772,12 +772,13 @@ let extract_pftreestate pts =
       (str"Cannot extract from a proof-tree in which we have descended;" ++
          spc () ++ str"Please ascend to the root");
   let pfterm,subgoals = extract_open_pftreestate pts in
-  let exl = Evd.non_instantiated pts.tpfsigma in
+  let exl = Evarutil.non_instantiated pts.tpfsigma in
   if subgoals <> [] or exl <> [] then
-   (if subgoals <> [] then
-     str "Attempt to save an incomplete proof"
-    else
-      str "Attempt to save a proof with existential variables still non-instantiated");
+    errorlabstrm "extract_proof"
+      (if subgoals <> [] then
+        str "Attempt to save an incomplete proof"
+      else
+        str "Attempt to save a proof with existential variables still non-instantiated");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
   strong whd_betaiotaevar env pts.tpfsigma pfterm
   (***
-- 
cgit v1.2.3