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

3 files changed, 4 insertions, 4 deletions

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.