aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetInterface.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetInterface.v')
-rw-r--r--theories/FSets/FSetInterface.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index d94ff7c95..8aede5527 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.