From fdb4e951e25d8e1a87c7ccc32acfdcf8d7737368 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 14 Dec 2000 07:42:27 +0000
Subject: LetIn dans Simpl

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

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8a6291c2d5..2108301c37 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -932,7 +932,7 @@ let injClause cls gls =
         with
 	  | Not_found ->
 	      errorlabstrm "InjClause" (not_found_message id)
-          | UserError("refiner__FAIL",_) -> 
+          | UserError("refiner__fail",_) -> 
               errorlabstrm "InjClause" 
 		[< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >]
 
-- 
cgit v1.2.3