From e964da1ad108e2bc1f5f01f4ad041c10a07f5d6f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 00:05:57 +0000
Subject: Message d'erreur

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4ecdfb66ac..fcf60e396e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -988,8 +988,8 @@ let try_rewrite tac gls =
 	errorlabstrm "try_rewrite" (str "Not a primitive equality here")
     | e when catchable_exception e -> 
 	errorlabstrm "try_rewrite"
-          (str "Cannot find a well type generalisation of the goal that" ++
-             str " makes progress the proof.")
+          (str "Cannot find a well-typed generalization of the goal that" ++
+             str " makes the proof progress")
 
 let subst l2r eqn cls gls =
   match cls with
-- 
cgit v1.2.3