- Module/Declare Module syntax made more uniform:

  * "Module X [binders] [:T] [:= b]." is now used to define a module both
    in module definitions and module type definitions. Moreover "b" can now
    be a functor application in every situation (this was not accepted for
    module definitions in module type definitions)
  * "Declare Module X : T." is now used to declare a module both in module
    definitions and module type definitions.
- Added syntactic sugar "Declare Module Export/Import" and
  "Module Export/Import"
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
  "Module Type M(Export/Import X Y: T)"
  (only for interactive definitions) (doc TODO)


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

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 97bb4fc8d..098ab23ff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,12 @@ Tactics
 Modules
 
 - Added "Locate Module qualid" to get the full path of a module.
+- Module/Declare Module syntax made more uniform (doc TODO)
+- Added syntactic sugar "Declare Module Export/Import" and
+  "Module Export/Import" (doc TODO)
+- Added syntactic sugar "Module M(Export/Import X Y: T)" and
+  "Module Type M(Export/Import X Y: T)"
+  (only for interactive definitions) (doc TODO)
 
 Notations