From c3870759a117b8dc66b759844ffa0ddd2fab58a4 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 26 Feb 2001 12:00:36 +0000
Subject: changement message d'erreur Abstract

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1405 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c92d80641a..82f4314456 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1699,7 +1699,7 @@ let abstract_subproof name tac gls =
   let concl = 
     List.fold_left (fun t d -> mkNamedProd_or_LetIn d t) (pf_concl gls) sign 
   in
-  if occur_existential concl then error "Cannot abstract with existentials";
+  if occur_existential concl then error "Abstract cannot handle existentials";
   let lemme =
     start_proof na Declare.NeverDischarge current_sign concl;
     let _,(const,strength) =
-- 
cgit v1.2.3