diff options
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 866c3f620..c2bba9283 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -125,7 +125,7 @@ Module Raw (X: DecidableType). Lemma In_eq : forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s. Proof. - intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto. + intros s x y; setoid_rewrite InA_alt; firstorder eauto. Qed. Hint Immediate In_eq. |