diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-12 11:28:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-12 11:28:14 +0000 |
| commit | 6bf05daa46ced26deec23c33590e9414d26d40e2 (patch) | |
| tree | a6992743030cd776b8817bae7e533deb15448cc5 /tactics/equality.ml | |
| parent | f30347427516e70bb720fc7ed1a08a4f055bae9e (diff) | |
Addendum to revision 12501.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index abf2e51c4..1979a0494 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 |