From 9b6517c0c933fb1d66c7feb53fa57e1697d8124a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 7 Jan 2010 15:32:49 +0000
Subject: 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
---
 theories/Numbers/Integer/Abstract/ZBase.v       | 2 +-
 theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9b5a80762f..44bb02ecc6 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 7f22532059..9b6f0ff644 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.
 
-- 
cgit v1.2.3