Update of theories/Numbers directory.

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

11 files changed, 32 insertions, 38 deletions

diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index 7d8fb573a6..ad17e5255e 100644
--- a/theories/Numbers/Natural/Axioms/NAxioms.v
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -174,7 +174,7 @@ Implicit Arguments recursion_S [A].
 
 End NatSignature.
 
-Module NatProperties (Import NatModule : NatSignature).
+Module NatProperties (Export NatModule : NatSignature).
 Module Export DomainPropertiesModule := DomainProperties DomainModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
index 1d35bfbc45..85ff0eb72b 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -1,6 +1,4 @@
-Require Import NAxioms.
-Require Import NPlus.
-Require Import NTimes.
+Require Export NTimes.
 
 (* Here we allow dependent recursion only for domains with Libniz
 equality. The reason is that, if the domain is A : nat -> Set, then (A
@@ -28,9 +26,10 @@ Axiom dep_recursion_S :
 
 End DepRecSignature.
 
-Module DepRecTimesProperties (Import DepRecModule : DepRecSignature)
-                             (Import TimesModule : TimesSignature
-                                with Module PlusModule.NatModule := DepRecModule.NatModule).
+Module DepRecTimesProperties
+  (Export DepRecModule : DepRecSignature)
+  (TimesModule : TimesSignature
+    with Module PlusModule.NatModule := DepRecModule.NatModule).
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
index 9dc8e4078b..de2ddf116e 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -61,7 +61,7 @@ Notation "x # y" := ((E x y) -> False) (at level 70) : NScope.
 
 End DomainEqSignature.
 
-Module DomainProperties (Import DomainModule : DomainSignature).
+Module DomainProperties (Export DomainModule : DomainSignature).
 (* It also accepts module of type NatDomainEq *)
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v
index fdf3418ed8..83bcf8ebea 100644
--- a/theories/Numbers/Natural/Axioms/NIso.v
+++ b/theories/Numbers/Natural/Axioms/NIso.v
@@ -1,4 +1,4 @@
-Require Import NAxioms.
+Require Export NAxioms.
 
 Module Homomorphism (Nat1 Nat2 : NatSignature).
 
diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v
index a70b3f95bf..254db11d65 100644
--- a/theories/Numbers/Natural/Axioms/NLt.v
+++ b/theories/Numbers/Natural/Axioms/NLt.v
@@ -14,8 +14,8 @@ Axiom lt_0 : forall x, ~ (x < 0).
 Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y.
 End LtSignature.
 
-Module LtProperties (Import LtModule : LtSignature).
-Module Import NatPropertiesModule := NatProperties NatModule.
+Module LtProperties (Export LtModule : LtSignature).
+Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
 Theorem lt_n_Sn : forall n, n < S n.
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 03f3cd86ec..38af96b1d0 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -1,11 +1,6 @@
-Require Import Bool. (* To get the negb function *)
-Require Import NAxioms.
-Require Import NStrongRec.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
+Require Export Bool. (* To get the negb function *)
+Require Export NStrongRec.
+Require Export NTimesLt.
 
 Module MiscFunctFunctor (NatMod : NatSignature).
 Module Export NatPropertiesModule := NatProperties NatMod.
@@ -318,7 +313,7 @@ Qed.
 End DefaultPlusModule.
 
 Module DefaultTimesModule <: TimesSignature.
-Module Import PlusModule := DefaultPlusModule.
+Module PlusModule := DefaultPlusModule.
 
 Definition times := times.
 
@@ -361,11 +356,11 @@ Qed.
 
 End DefaultLtModule.
 
-Module Import DefaultPlusProperties := PlusProperties DefaultPlusModule.
-Module Import DefaultTimesProperties := TimesProperties DefaultTimesModule.
-Module Import DefaultLtProperties := LtProperties DefaultLtModule.
-Module Import DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
-Module Import DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
+Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule.
+Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule.
+Module Export DefaultLtProperties := LtProperties DefaultLtModule.
+Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
+Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
 
 (*Opaque MiscFunctFunctor.plus.
 Check plus_comm. (* This produces the following *)
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index d2ef810181..63cc8a40f5 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -17,7 +17,7 @@ Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m).
 
 End PlusSignature.
 
-Module PlusProperties (Import PlusModule : PlusSignature).
+Module PlusProperties (Export PlusModule : PlusSignature).
 Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v
index 77bd800122..3724f9ec50 100644
--- a/theories/Numbers/Natural/Axioms/NPlusLt.v
+++ b/theories/Numbers/Natural/Axioms/NPlusLt.v
@@ -1,8 +1,8 @@
 Require Export NPlus.
 Require Export NLt.
 
-Module PlusLtProperties (Import PlusModule : PlusSignature)
-                        (Import LtModule : LtSignature with
+Module PlusLtProperties (PlusModule : PlusSignature)
+                        (LtModule : LtSignature with
                            Module NatModule := PlusModule.NatModule).
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Module Export LtPropertiesModule := LtProperties LtModule.
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v
index 5e8223108c..a2e73f99ac 100644
--- a/theories/Numbers/Natural/Axioms/NStrongRec.v
+++ b/theories/Numbers/Natural/Axioms/NStrongRec.v
@@ -1,7 +1,7 @@
-Require Import NAxioms.
+Require Export NAxioms.
 
-Module StrongRecProperties (Import NatModule : NatSignature).
-Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule.
+Module StrongRecProperties (NatModule : NatSignature).
+Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
 Section StrongRecursion.
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index 6a7e9ba39e..4d1d2b0cad 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -15,7 +15,7 @@ Axiom times_Sn_m : forall n m, (S n) * m == m + n * m.
 
 End TimesSignature.
 
-Module TimesProperties (Import TimesModule : TimesSignature).
+Module TimesProperties (Export TimesModule : TimesSignature).
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v
index c728f05a83..36989f1b3c 100644
--- a/theories/Numbers/Natural/Axioms/NTimesLt.v
+++ b/theories/Numbers/Natural/Axioms/NTimesLt.v
@@ -1,13 +1,13 @@
-Require Export NLt.
 Require Export NTimes.
 Require Export NPlusLt.
 
-Module TimesLtProperties (Import TimesModule : TimesSignature)
-                         (Import LtModule : LtSignature with
+Module TimesLtProperties (TimesModule : TimesSignature)
+                         (LtModule : LtSignature with
                             Module NatModule := TimesModule.PlusModule.NatModule).
-Module Export TimesPropertiesModule := TimesProperties TimesModule.
-Module Export LtPropertiesModule := LtProperties LtModule.
-Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule.
+Module Export TimesPropertiesModule :=
+  TimesProperties TimesModule.
+Module Export PlusLtPropertiesModule :=
+  PlusLtProperties TimesModule.PlusModule LtModule.
 Open Local Scope NScope.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.