summaryrefslogtreecommitdiff
path: root/theories/Structures/OrdersLists.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/OrdersLists.v')
-rw-r--r--theories/Structures/OrdersLists.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 2ed07026..f83b6377 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -86,11 +86,11 @@ Module KeyOrderedType(Import O:OrderedType).
(* eqk, eqke are equalities, ltk is a strict order *)
- Global Instance eqk_equiv : Equivalence eqk.
+ Global Instance eqk_equiv : Equivalence eqk := _.
- Global Instance eqke_equiv : Equivalence eqke.
+ Global Instance eqke_equiv : Equivalence eqke := _.
- Global Instance ltk_strorder : StrictOrder ltk.
+ Global Instance ltk_strorder : StrictOrder ltk := _.
Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
Proof. unfold eqk, ltk; auto with *. Qed.