diff options
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 *) |