summaryrefslogtreecommitdiff
path: root/theories/MSets/MSetWeakList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSetWeakList.v')
-rw-r--r--theories/MSets/MSetWeakList.v4
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 945cb2dd..76f09c76 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id$ *)
-
(** * Finite sets library *)
(** This file proposes an implementation of the non-dependant
@@ -517,7 +515,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
Definition In := InA X.eq.
Definition eq := Equal.
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
End MakeRaw.