From 11ef6b79e5d5b3dd0c46829040f417bd364b9a2d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 29 Apr 2005 18:31:15 +0000
Subject: Protection against saving a proof with still non-instantiated evars
 (cf bug #901)

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

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index cd592296d3..804d009b14 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -772,9 +772,12 @@ 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
-  if subgoals <> [] then
-   errorlabstrm "extract_proof"
-   (str "Attempt to save an incomplete proof");
+  let exl = Evd.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");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
   strong whd_betaiotaevar env pts.tpfsigma pfterm
   (***
-- 
cgit v1.2.3