- 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, 2 insertions, 2 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index ddcfd1bcd..57be3dbdf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -450,7 +450,7 @@ let intern_args interp_modtype (env,oldargs) (idl,arg) =
     in
     env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
       
-let start_module interp_modtype id args res_o =
+let start_module interp_modtype export id args res_o =
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
   let env,arg_entries_revlist = 
@@ -482,7 +482,7 @@ let start_module interp_modtype id args res_o =
 
   let mbids = List.map fst arg_entries in
   openmod_info:=(mbids,res_entry_o,sub_body_o);
-  let prefix = Lib.start_module id mp fs in
+  let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
   Lib.add_frozen_state ()