Numbers: separation of funs, notations, axioms. Notations via module, without scope.

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

11 files changed, 21 insertions, 31 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index c3e1e223e1..9f0b54a6a2 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -12,11 +12,9 @@
 
 Require Export NBase.
 
-Module NAddPropFunct (Import N : NAxiomsSig).
+Module NAddPropFunct (Import N : NAxiomsSig').
 Include NBasePropFunct N.
 
-Local Open Scope NumScope.
-
 (** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *)
 (** Now comes theorems valid for natural numbers but not for Z *)
 
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index f48b62e614..0ce04e54eb 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -12,9 +12,8 @@
 
 Require Export NOrder.
 
-Module NAddOrderPropFunct (Import N : NAxiomsSig).
+Module NAddOrderPropFunct (Import N : NAxiomsSig').
 Include NOrderPropFunct N.
-Local Open Scope NumScope.
 
 (** Theorems true for natural numbers, not for integers *)
 
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 1cb4746741..42016ab10b 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -14,9 +14,7 @@ Require Export NZAxioms.
 
 Set Implicit Arguments.
 
-Module Type NAxiomsSig.
-Include Type NZOrdAxiomsSig.
-Local Open Scope NumScope.
+Module Type NAxioms (Import NZ : NZDomainSig').
 
 Axiom pred_0 : P 0 == 0.
 
@@ -34,5 +32,8 @@ Axiom recursion_succ :
     Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
-End NAxiomsSig.
+End NAxioms.
+
+Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms.
+Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 4095fbb502..0d489a16d7 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -14,10 +14,9 @@ Require Export Decidable.
 Require Export NAxioms.
 Require Import NZProperties.
 
-Module NBasePropFunct (Import N : NAxiomsSig).
+Module NBasePropFunct (Import N : NAxiomsSig').
 (** First, we import all known facts about both natural numbers and integers. *)
 Include Type NZPropFunct N.
-Local Open Scope NumScope.
 
 (** We prove that the successor of a number is not zero by defining a
 function (by recursion) that maps 0 to false and the successor to true *)
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 69dbf656e3..8ac7c6f6db 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -14,9 +14,8 @@ Require Import Bool. (* To get the orb and negb function *)
 Require Import RelationPairs.
 Require Export NStrongRec.
 
-Module NdefOpsPropFunct (Import N : NAxiomsSig).
+Module NdefOpsPropFunct (Import N : NAxiomsSig').
 Include NStrongRecPropFunct N.
-Local Open Scope NumScope.
 
 (*****************************************************)
 (**                   Addition                       *)
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 9e446dc69a..dd033fb764 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -10,16 +10,14 @@
 
 Require Import NAxioms NProperties NZDiv.
 
-Open Scope NumScope.
-
-Module Type NDiv (Import N : NAxiomsSig).
- Include Type NZDivCommon N. (** div, mod, compat with eq, equation a=bq+r *)
+Module Type NDivSpecific (Import N : NAxiomsSig')(Import DM : DivMod' N).
  Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
-End NDiv.
+End NDivSpecific.
 
-Module Type NDivSig := NAxiomsSig <+ NDiv.
+Module Type NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific.
+Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
 
-Module NDivPropFunct (Import N : NDivSig)(Import NP : NPropSig N).
+Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N).
 
 (** We benefit from what already exists for NZ *)
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 13e289c295..47bf38cbaf 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -17,10 +17,10 @@ Module Homomorphism (N1 N2 : NAxiomsSig).
 Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).
 
 Definition homomorphism (f : N1.t -> N2.t) : Prop :=
-  f N1.zero == N2.zero /\ forall n, f (N1.S n) == N2.S (f n).
+  f N1.zero == N2.zero /\ forall n, f (N1.succ n) == N2.succ (f n).
 
 Definition natural_isomorphism : N1.t -> N2.t :=
-  N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.S p).
+  N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.succ p).
 
 Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.
 Proof.
@@ -38,7 +38,7 @@ unfold natural_isomorphism; now rewrite N1.recursion_0.
 Qed.
 
 Theorem natural_isomorphism_succ :
-  forall n : N1.t, natural_isomorphism (N1.S n) == N2.S (natural_isomorphism n).
+  forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
 intro n. rewrite N1.recursion_succ; auto with *.
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 285d8c1049..a2162b137f 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -12,9 +12,8 @@
 
 Require Export NAddOrder.
 
-Module NMulOrderPropFunct (Import N : NAxiomsSig).
+Module NMulOrderPropFunct (Import N : NAxiomsSig').
 Include NAddOrderPropFunct N.
-Local Open Scope NumScope.
 
 (** Theorems that are either not valid on Z or have different proofs
     on N and Z *)
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 94c68a1867..090c02ecf6 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -12,9 +12,8 @@
 
 Require Export NAdd.
 
-Module NOrderPropFunct (Import N : NAxiomsSig).
+Module NOrderPropFunct (Import N : NAxiomsSig').
 Include NAddPropFunct N.
-Local Open Scope NumScope.
 
 (* Theorems that are true for natural numbers but not for integers *)
 
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 7629aa11b2..ed867b8250 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -15,9 +15,8 @@ and proves its properties *)
 
 Require Export NSub.
 
-Module NStrongRecPropFunct (Import N : NAxiomsSig).
+Module NStrongRecPropFunct (Import N : NAxiomsSig').
 Include Type NSubPropFunct N.
-Local Open Scope NumScope.
 
 Section StrongRecursion.
 
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index e027c0be2e..bc638cf3b6 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -12,9 +12,8 @@
 
 Require Export NMulOrder.
 
-Module Type NSubPropFunct (Import N : NAxiomsSig).
+Module Type NSubPropFunct (Import N : NAxiomsSig').
 Include NMulOrderPropFunct N.
-Local Open Scope NumScope.
 
 Theorem sub_0_l : forall n, 0 - n == 0.
 Proof.