Description of the new features of the module system (first part).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12587 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index be86cd7ba6..9867a7e21a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -87,6 +87,9 @@ Vernacular commands
   congruence schemes available to user (governed by options "Unset
   Case Analysis Schemes" and "Unset Congruence Schemes").
 - Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
+- New commands for modules and module types "Include Self <module_expr>"  and 
+  "Include Type Self <modtype_expr>".
+
 
 Tools
 
@@ -134,6 +137,14 @@ Library
   - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated;
   - new file Sorted.v for some definitions of being sorted.
 
+Language
+
+- New implementation of the module system. The sharing between non-logical
+  object and the management of the name-space has been improved by the new 
+  \Delta-equivalence on qualified name. The include operator has been extended 
+  to high-order structures (cf. libraries Numbers ans Structures to see examples).
+  Interactive proofs are now authorized in module type.
+
 Changes from V8.1 to V8.2
 =========================