From 6bf05daa46ced26deec23c33590e9414d26d40e2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 12 Nov 2009 11:28:14 +0000
Subject: Addendum to revision 12501.

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index abf2e51c4e..1979a04946 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -179,7 +179,7 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
 
 let find_elim hdcncl lft2rgt dep cls gl =
   let inccl = (cls = None) in
-  if hdcncl = constr_of_reference (Coqlib.glob_eq) then
+  if hdcncl = constr_of_reference (Coqlib.glob_eq) & not dep then
     (* use eq_rect, eq_rect_r, etc for compatibility *)
     let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
     let hdcncls = string_of_inductive hdcncl ^ suffix in
-- 
cgit v1.2.3