diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /theories/Structures/OrdersEx.v | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
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 *) |