8 files changed, 24 insertions, 33 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 785abb5c7..bca7c3682 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -13,7 +13,8 @@
 Require Import NZAxioms.
 Require Import NZBase.
 
-Module NZAddProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
+Module Type NZAddPropSig
+ (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
 Local Open Scope NumScope.
 
 Hint Rewrite
@@ -88,6 +89,4 @@ Proof.
 intro n; now nzsimpl.
 Qed.
 
-End NZAddProp.
-
-Module NZAddPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZAddProp NZ.
+End NZAddPropSig.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index b51216fd2..56982c616 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -12,10 +12,8 @@
 
 Require Import NZAxioms NZBase NZMul NZOrder.
 
-Module NZAddOrderProp
- (Import NZ : NZOrdAxiomsSig)(Import NZBase : NZBaseProp NZ).
-Include NZMulProp NZ NZBase.
-Include NZOrderProp NZ NZBase.
+Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig).
+Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
 Local Open Scope NumScope.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
@@ -152,8 +150,5 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-End NZAddOrderProp.
-
-Module NZAddOrderPropFunct (NZ:NZOrdAxiomsSig) :=
- NZBasePropFunct NZ <+ NZAddOrderProp NZ.
+End NZAddOrderPropSig.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 1215bfba2..04955b3b3 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,7 +12,7 @@
 
 Require Import NZAxioms.
 
-Module Type NZBaseProp (Import NZ : NZDomainSig).
+Module Type NZBasePropSig (Import NZ : NZDomainSig).
 Local Open Scope NumScope.
 
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
@@ -86,9 +86,5 @@ Tactic Notation "nzinduct" ident(n) :=
 Tactic Notation "nzinduct" ident(n) constr(u) :=
   induction_maker n ltac:(apply central_induction with (z := u)).
 
-End NZBaseProp.
-
-Module NZBasePropFunct (NZ : NZDomainSig).
- Include Type NZBaseProp NZ.
-End NZBasePropFunct.
+End NZBasePropSig.
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 5b81cadd2..db64a7963 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -38,9 +38,8 @@ End NZDiv.
 
 Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv.
 
-Module NZDivPropFunct (Import NZ : NZDivSig).
- (* TODO: a transformer un jour en arg funct puis include *)
- Module Import P := NZMulOrderPropFunct NZ.
+Module NZDivPropFunct
+ (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ).
 
 (** Uniqueness theorems *)
 
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 0daca2b87..e7c9b05e0 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -12,8 +12,9 @@
 
 Require Import NZAxioms NZBase NZAdd.
 
-Module NZMulProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
-Include NZAddProp NZ NZBase.
+Module Type NZMulPropSig
+ (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
+Include Type NZAddPropSig NZ NZBase.
 Local Open Scope NumScope.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
@@ -67,6 +68,4 @@ Proof.
 intro n. now nzsimpl.
 Qed.
 
-End NZMulProp.
-
-Module NZMulPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZMulProp NZ.
+End NZMulPropSig.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index b6e4849f5..a4d8a3972 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -13,8 +13,8 @@
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
-Module NZMulOrderPropFunct (Import NZ : NZOrdAxiomsSig).
-Include NZAddOrderPropFunct NZ.
+Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig).
+Include Type NZAddOrderPropSig NZ.
 Local Open Scope NumScope.
 
 Theorem mul_lt_pred :
@@ -305,4 +305,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l.
 apply add_pos_pos; now apply lt_0_1.
 Qed.
 
-End NZMulOrderPropFunct.
+End NZMulOrderPropSig.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index c6815ebf5..a95de8df7 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -12,7 +12,8 @@
 
 Require Import NZAxioms NZBase Decidable OrderTac.
 
-Module NZOrderProp (Import NZ : NZOrdSig)(Import NZBase : NZBaseProp NZ).
+Module Type NZOrderPropSig
+ (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ).
 Local Open Scope NumScope.
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -613,9 +614,11 @@ Qed.
 
 End WF.
 
-End NZOrderProp.
+End NZOrderPropSig.
 
-Module NZOrderPropFunct (NZ : NZOrdSig) := NZBasePropFunct NZ <+ NZOrderProp NZ.
+Module NZOrderPropFunct (Import NZ : NZOrdSig).
+ Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
+End NZOrderPropFunct.
 
 
 (** To Merge with GenericMinMax ... *)
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 781d06594..125b4f62c 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -17,4 +17,4 @@ Require Export NZAxioms NZMulOrder.
     subsumes all others.
 *)
 
-Module NZPropFunct := NZMulOrderPropFunct.
+Module Type NZPropFunct := NZMulOrderPropSig.