An update on axiomatization of number classes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 17 deletions

diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 77fbdcaf7f..f87baf687c 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -2,12 +2,13 @@ Require Import NArith.
 Require Import Ndec.
 
 Require Export NDepRec.
-Require Export NTimesLt.
+Require Export NTimesOrder.
+Require Export NMinus.
 Require Export NMiscFunct.
 
 Open Local Scope N_scope.
 
-Module BinaryDomain : DomainEqSignature
+Module NBinaryDomain : NDomainEqSignature
   with Definition N := N
   with Definition E := (@eq N)
   with Definition e := Neqb.
@@ -31,11 +32,10 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-End BinaryDomain.
+End NBinaryDomain.
 
 Module BinaryNat <: NatSignature.
-
-Module Export DomainModule := BinaryDomain.
+Module Export NDomainModule := NBinaryDomain.
 
 Definition O := N0.
 Definition S := Nsucc.
@@ -92,8 +92,8 @@ Qed.
 
 End BinaryNat.
 
-Module BinaryDepRec <: DepRecSignature.
-Module Export DomainModule := BinaryDomain.
+Module NBinaryDepRec <: NDepRecSignature.
+Module Export NDomainModule := NBinaryDomain.
 Module Export NatModule := BinaryNat.
 
 Definition dep_recursion := Nrec.
@@ -112,10 +112,9 @@ Proof.
 intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step.
 Qed.
 
-End BinaryDepRec.
-
-Module BinaryPlus <: PlusSignature.
+End NBinaryDepRec.
 
+Module NBinaryPlus <: NPlusSignature.
 Module Export NatModule := BinaryNat.
 
 Definition plus := Nplus.
@@ -135,10 +134,10 @@ Proof.
 exact Nplus_succ.
 Qed.
 
-End BinaryPlus.
+End NBinaryPlus.
 
-Module BinaryTimes <: TimesSignature.
-Module Export PlusModule := BinaryPlus.
+Module NBinaryTimes <: NTimesSignature.
+Module Export NPlusModule := NBinaryPlus.
 
 Definition times := Nmult.
 
@@ -157,9 +156,9 @@ Proof.
 exact Nmult_Sn_m.
 Qed.
 
-End BinaryTimes.
+End NBinaryTimes.
 
-Module BinaryLt <: LtSignature.
+Module NBinaryLt <: NLtSignature.
 Module Export NatModule := BinaryNat.
 
 Definition lt (m n : N) := less_than (Ncompare m n).
@@ -184,9 +183,9 @@ assert (H2 : lt x y <-> Ncompare x y = Lt);
 pose proof (Ncompare_n_Sm x y) as H. tauto.
 Qed.
 
-End BinaryLt.
+End NBinaryLt.
 
-Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt.
+Module Export NBinaryTimesLtProperties := NTimesLtProperties NBinaryTimes NBinaryLt.
 
 (*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)