From d3ac30ae99a9e56bdf0718487a4607e1fae79242 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 13 Mar 2007 14:45:21 +0000
Subject: Correction bug #1439 (comportement de replace by)

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

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index a9a869d8f7..9ca5dabdcb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -189,7 +189,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
   let try_prove_eq = 
     match try_prove_eq_opt with 
       | None -> tclIDTAC
-      | Some tac ->  tclTRY (tclCOMPLETE tac)
+      | Some tac ->  tclCOMPLETE tac
   in
   let t1 = pf_apply get_type_of gl c1 
   and t2 = pf_apply get_type_of gl c2 in
-- 
cgit v1.2.3