From 3845ef57ee0d87e0730fa66ed3313360f1f8780d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Mar 2004 22:31:18 +0000
Subject: ne pas échouer si but inchangé pour préserver la compatibilité de
 'replace'

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2f36d0c7ef..cabbdba869 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -137,7 +137,9 @@ let abstract_replace clause c2 c1 unsafe gl =
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
-	tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id]));
+	tclTHEN 
+	  (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
+	  (clear [id]));
        tclORELSE assumption 
 	(tclTRY (tclTHEN (apply sym) assumption))] gl
   else
-- 
cgit v1.2.3