4 files changed, 5 insertions, 6 deletions
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 7313c4131c..97c122029f 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -13,7 +13,7 @@
 Require Import NZAxioms NZBase NZMul NZOrder.
 
 Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
+Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 3c11024e52..296bd095f9 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -14,7 +14,7 @@ Require Import NZAxioms NZBase NZAdd.
 
 Module Type NZMulPropSig
  (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
-Include Type NZAddPropSig NZ NZBase.
+Include NZAddPropSig NZ NZBase.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 18f61de598..7b64a69836 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -14,7 +14,7 @@ Require Import NZAxioms.
 Require Import NZAddOrder.
 
 Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZAddOrderPropSig NZ.
+Include NZAddOrderPropSig NZ.
 
 Theorem mul_lt_pred :
   forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 6697c0b3dc..6a086f3bd6 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -611,7 +611,6 @@ End WF.
 
 End NZOrderPropSig.
 
-Module NZOrderPropFunct (Import NZ : NZOrdSig).
- Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
-End NZOrderPropFunct.
+Module NZOrderPropFunct (NZ : NZOrdSig) :=
+ NZBasePropSig NZ <+ NZOrderPropSig NZ.