diff options
Diffstat (limited to 'theories/Classes/Equivalence.v')
| -rw-r--r-- | theories/Classes/Equivalence.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 00519ecf4..a4c97fc82 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -109,8 +109,8 @@ Ltac equiv_simplify := repeat equiv_simplify_one. Ltac equivify_tac := match goal with - | [ s : Equivalence ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H - | [ s : Equivalence ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) + | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H + | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) end. Ltac equivify := repeat equivify_tac. |