diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
commit | 9b6517c0c933fb1d66c7feb53fa57e1697d8124a (patch) | |
tree | d914d6bc2c5598baad03807ce40ada0b1d56045d /theories/FSets/FSetInterface.v | |
parent | e3e6ff629e258269bc9fe06f7be99a2d5f334071 (diff) |
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
Diffstat (limited to 'theories/FSets/FSetInterface.v')
-rw-r--r-- | theories/FSets/FSetInterface.v | 6 |
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. |