summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetCompat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetCompat.v')
-rw-r--r--theories/FSets/FSetCompat.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index c3d614ee..6b3d86d3 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -264,7 +264,7 @@ Module Update_WSets
Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In.
Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed.
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
Section Spec.
Variable s s': t.