From 157bee13827f9a616b6c82be4af110c8f2464c64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 May 2011 15:12:23 +0000
Subject: Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Structures/OrdersEx.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Structures')

diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index ffc5b91bca..2cb591968d 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -21,7 +21,7 @@ Require Import Orders NPeano POrderedType NArith
 
 Module Nat_as_OT := NPeano.Nat.
 Module Positive_as_OT := POrderedType.Positive_as_OT.
-Module N_as_OT := NArith.N.
+Module N_as_OT := BinNat.N.
 Module Z_as_OT := ZBinary.Z.
 
 (** An OrderedType can now directly be seen as a DecidableType *)
-- 
cgit v1.2.3