diff options
| author | Guillaume Melquiond | 2016-01-05 20:07:37 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-05 20:07:37 +0100 |
| commit | 7ca0319268c2c6912e08c53deb742d5f7631e210 (patch) | |
| tree | 5c9613224ca234af907374485b6f2241303e23ee /theories/Structures | |
| parent | 5d26829704b2602ede45183cba54ab219e453c0e (diff) | |
| parent | e4a682e2f2c91fac47f55cd8619af2321b2e4c30 (diff) | |
Merge remote-tracking branch 'origin/v8.5' into trunk
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 88fbd8c11c..954d3df203 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<x. |