diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
| commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/Structures/OrdersEx.v | |
| parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/Structures/OrdersEx.v')
| -rw-r--r-- | theories/Structures/OrdersEx.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index 9f83d82b..e071d053 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -11,20 +11,18 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrdersEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) - -Require Import Orders NatOrderedType POrderedType NOrderedType - ZOrderedType RelationPairs EqualitiesFacts. +Require Import Orders NPeano POrderedType NArith + ZArith RelationPairs EqualitiesFacts. (** * Examples of Ordered Type structures. *) (** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) -Module Nat_as_OT := NatOrderedType.Nat_as_OT. +Module Nat_as_OT := NPeano.Nat. Module Positive_as_OT := POrderedType.Positive_as_OT. -Module N_as_OT := NOrderedType.N_as_OT. -Module Z_as_OT := ZOrderedType.Z_as_OT. +Module N_as_OT := BinNat.N. +Module Z_as_OT := BinInt.Z. (** An OrderedType can now directly be seen as a DecidableType *) |