From e2b35440ac709a3702ff30ab74c4a324e75929b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Jul 2008 16:10:45 +0000
Subject: - Rebranchement backtrack du langage déclaratif dans Coqide - Divers:
 message d'erreur et typo relatifs au langage déclaratif

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

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1afd45b1f4..1ad7dcd0ad 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -754,9 +754,7 @@ let extract_open_pftreestate pts =
 
 let extract_pftreestate pts =
   if pts.tstack <> [] then
-    errorlabstrm "extract_pftreestate"
-      (str"Cannot extract from a proof-tree in which we have descended;" ++
-         spc () ++ str"Please ascend to the root");
+    errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed");
   let pfterm,subgoals = extract_open_pftreestate pts in
   let exl = Evarutil.non_instantiated pts.tpfsigma in
   if subgoals <> [] or exl <> [] then
-- 
cgit v1.2.3