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.