aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersFacts.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/OrdersFacts.v')
-rw-r--r--theories/Structures/OrdersFacts.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index a28b79776..b328ae2e8 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -208,7 +208,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
Definition t := O.t.
Definition eq := O.eq.
-Instance eq_equiv : Equivalence eq.
+Program Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.
Definition lt := flip O.lt.