Include can accept both Module and Module Type

 Syntax Include Type is still active, but deprecated, and triggers a warning.
 The syntax M <+ M' <+ M'', which performs internally an Include, also
 benefits from this: M, M', M'' can be independantly modules or module type.

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

15 files changed, 29 insertions, 30 deletions

diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index cd51b2affe..e60cca9d97 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -258,7 +258,7 @@ End WSfun.
 
 Module Type WS.
   Declare Module E : DecidableType.
-  Include Type WSfun E.
+  Include WSfun E.
 End WS.
 
 
@@ -266,7 +266,7 @@ End WS.
 (** ** Maps on ordered keys, functorial signature *)
 
 Module Type Sfun (E : OrderedType).
-  Include Type WSfun E.
+  Include WSfun E.
   Section elt.
   Variable elt:Type.
    Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
@@ -284,7 +284,7 @@ End Sfun.
 
 Module Type S.
   Declare Module E : OrderedType.
-  Include Type Sfun E.
+  Include Sfun E.
 End S.
 
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index d94ff7c95d..8aede55272 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -275,7 +275,7 @@ End WSfun.
 
 Module Type WS.
   Declare Module E : DecidableType.
-  Include Type WSfun E.
+  Include WSfun E.
 End WS.
 
 
@@ -286,7 +286,7 @@ End WS.
     and some stronger specifications for other functions. *)
 
 Module Type Sfun (E : OrderedType).
-  Include Type WSfun E.
+  Include WSfun E.
 
   Parameter lt : t -> t -> Prop.
   Parameter compare : forall s s' : t, Compare lt eq s s'.
@@ -349,7 +349,7 @@ End Sfun.
 
 Module Type S.
   Declare Module E : OrderedType.
-  Include Type Sfun E.
+  Include Sfun E.
 End S.
 
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index effd5e35a9..cb18785e6c 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -117,7 +117,7 @@ End HasWOps.
 Module Type WOps (E : DecidableType).
   Definition elt := E.t.
   Parameter t : Type. (** the abstract type of sets *)
-  Include Type HasWOps.
+  Include HasWOps.
 End WOps.
 
 
@@ -128,7 +128,7 @@ End WOps.
 
 Module Type WSetsOn (E : DecidableType).
   (** First, we ask for all the functions *)
-  Include Type WOps E.
+  Include WOps E.
 
   (** Logical predicates *)
   Parameter In : elt -> t -> Prop.
@@ -144,8 +144,8 @@ Module Type WSetsOn (E : DecidableType).
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq : t -> t -> Prop := Equal.
-  Include Type IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
-  Include Type HasEqDec.
+  Include IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
+  Include HasEqDec.
 
   (** Specifications of set operators *)
 
@@ -197,7 +197,7 @@ End WSetsOn.
 
 Module Type WSets.
   Declare Module E : DecidableType.
-  Include Type WSetsOn E.
+  Include WSetsOn E.
 End WSets.
 
 (** ** Functorial signature for sets on ordered elements
@@ -226,7 +226,7 @@ Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.
 
 
 Module Type SetsOn (E : OrderedType).
-  Include Type WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+  Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
 
   Section Spec.
   Variable s s': t.
@@ -266,7 +266,7 @@ End SetsOn.
 
 Module Type Sets.
   Declare Module E : OrderedType.
-  Include Type SetsOn E.
+  Include SetsOn E.
 End Sets.
 
 Module Type S := Sets.
@@ -335,7 +335,7 @@ Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
 
 Module Type WRawSets (E : DecidableType).
   (** First, we ask for all the functions *)
-  Include Type WOps E.
+  Include WOps E.
 
   (** Is a set well-formed or ill-formed ? *)
 
@@ -559,7 +559,7 @@ End WRaw2Sets.
 (** Same approach for ordered sets *)
 
 Module Type RawSets (E : OrderedType).
-  Include Type WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+  Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
 
   Section Spec.
   Variable s s': t.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9b5a80762f..44bb02ecc6 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
 Require Import NZProperties.
 
 Module ZBasePropFunct (Import Z : ZAxiomsSig').
-Include Type NZPropFunct Z.
+Include NZPropFunct Z.
 
 (* Theorems that are true for integers but not for natural numbers *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 7f22532059..9b6f0ff644 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -18,6 +18,6 @@ Require Export ZAxioms ZMulOrder.
 Module Type ZPropSig := ZMulOrderPropFunct.
 
 Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
- Include Type ZPropSig Z.
+ Include ZPropSig Z.
 End ZPropFunct.
 
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.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0d489a16d7..842f4bcf23 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -16,7 +16,7 @@ Require Import NZProperties.
 
 Module NBasePropFunct (Import N : NAxiomsSig').
 (** First, we import all known facts about both natural numbers and integers. *)
-Include Type NZPropFunct N.
+Include NZPropFunct N.
 
 (** 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/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 2baed54cfe..30262bd9f4 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -18,5 +18,5 @@ Require Export NAxioms NSub.
 Module Type NPropSig := NSubPropFunct.
 
 Module NPropFunct (N:NAxiomsSig) <: NPropSig N.
- Include Type NPropSig N.
+ Include NPropSig N.
 End NPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index ed867b8250..cbbcdbff50 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -16,7 +16,7 @@ and proves its properties *)
 Require Export NSub.
 
 Module NStrongRecPropFunct (Import N : NAxiomsSig').
-Include Type NSubPropFunct N.
+Include NSubPropFunct N.
 
 Section StrongRecursion.
 
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 43df377c08..2465dc539e 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -53,7 +53,7 @@ Local Infix "+" := trans_ord.
 Module Type TotalOrder_NoInline <: TotalOrder.
  Parameter Inline t : Type.
  Parameters eq lt le : t -> t -> Prop.
- Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
+ Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
 End TotalOrder_NoInline.
 
 Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
@@ -302,7 +302,7 @@ Definition t := O.t.
 Definition eq := O.eq.
 Definition lt := flip O.lt.
 Definition le := flip O.le.
-Include Type EqLtLeNotation.
+Include EqLtLeNotation.
 
 Instance eq_equiv : Equivalence eq.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index ca441fc867..1f3e50dc3f 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -41,7 +41,7 @@ Module Type MiniOrderedType.
 End MiniOrderedType.
 
 Module Type OrderedType.
-  Include Type MiniOrderedType.
+  Include MiniOrderedType.
 
   (** A [eq_dec] can be deduced from [compare] below. But adding this
      redundant field allows to see an OrderedType as a DecidableType. *)
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 1cddfea3b1..766b0faf05 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -43,7 +43,7 @@ Module Type LeNotation (E:EqLe).
 End LeNotation.
 
 Module Type LtLeNotation (E:EqLtLe).
-  Include Type LtNotation E <+ LeNotation E.
+  Include LtNotation E <+ LeNotation E.
   Notation "x <= y < z" := (x<=y /\ y<z).
   Notation "x < y <= z" := (x<y /\ y<=z).
 End LtLeNotation.