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

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index fb4e921d10..be8b1404a5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,8 @@ Vernacular commands
 - Declaring axiomatic type class instances in Module Type should be now
   done via new command "Declare Instance", while the syntax "Instance"
   now always provides a concrete instance, both in and out of Module Type.
+- Include Type is now deprecated since Include now accept both modules and
+  module types. 
 
 Tools