- 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

0 files changed, 0 insertions, 0 deletions