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/Numbers/Integer | |
| 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/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 9b5a80762..44bb02ecc 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 7f2253205..9b6f0ff64 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. |