From 3453438833ff72ad991e0691207481cb6682f246 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 9 Feb 2010 17:44:39 +0000 Subject: NBinary improved, contains more, subsumes NOrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/OrdersEx.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index d7c0deb94..90840ce1f 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -13,8 +13,8 @@ (* $Id$ *) -Require Import Orders NatOrderedType POrderedType NOrderedType - ZBinary RelationPairs EqualitiesFacts. +Require Import Orders NatOrderedType POrderedType NArith + ZArith RelationPairs EqualitiesFacts. (** * Examples of Ordered Type structures. *) @@ -23,8 +23,8 @@ Require Import Orders NatOrderedType POrderedType NOrderedType Module Nat_as_OT := NatOrderedType.Nat_as_OT. Module Positive_as_OT := POrderedType.Positive_as_OT. -Module N_as_OT := NOrderedType.N_as_OT. -Module Z_as_OT := ZBinary.Z. +Module N_as_OT := NArith.N. +Module Z_as_OT := ZArith.Z. (** An OrderedType can now directly be seen as a DecidableType *) -- cgit v1.2.3