From 37cc37090fcbabb9546a79558c9420e532701be4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Dec 2015 20:07:06 +0100 Subject: Put implicits back as in 8.4. --- theories/Structures/OrdersFacts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Structures') diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 88fbd8c11..954d3df20 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). Instance le_order : PartialOrder eq le. Proof. compute; iorder. Qed. - Instance le_antisym : Antisymmetric eq le. + Instance le_antisym : Antisymmetric _ eq le. Proof. apply partial_order_antisym; auto with *. Qed. Lemma le_not_gt_iff : forall x y, x<=y <-> ~y