Skip to content

Commit e04ba49

Browse files
author
Gregory Malecha
committed
don't add a rewrite for symmetry.
1 parent 28cafe6 commit e04ba49

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

theories/Data/Eq.v

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ Lemma eq_sym_eq
1717
Proof.
1818
destruct pf. reflexivity.
1919
Qed.
20-
Hint Rewrite eq_sym_eq : eq_rw.
2120

2221
Lemma match_eq_sym_eq
2322
: forall T (a b : T) (pf : a = b) F X,

0 commit comments

Comments
 (0)