- 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

4 files changed, 11 insertions, 12 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index ddcfd1bcd4..57be3dbdf4 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 ()
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index be9953f439..17a97e7aee 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -43,9 +43,8 @@ val declare_module :
   'modexpr option -> unit
  
 val start_module : (env -> 'modtype -> module_type_entry) -> 
-  identifier -> 
-  (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
-  unit
+  bool option -> identifier -> (identifier located list * 'modtype) list ->
+   ('modtype * bool) option -> unit
 
 val end_module : identifier -> unit
 
diff --git a/library/lib.ml b/library/lib.ml
index 16521e627b..980fd7e4ca 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -21,7 +21,7 @@ open Summary
 type node = 
   | Leaf of obj
   | CompilingLibrary of object_prefix
-  | OpenedModule of object_prefix * Summary.frozen
+  | OpenedModule of bool option * object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
@@ -125,7 +125,7 @@ let sections_are_opened () =
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection (dir,_)) :: _ -> dir
-    | (sp, OpenedModule (dir,_)) :: _ -> dir
+    | (sp, OpenedModule (_,dir,_)) :: _ -> dir
     | (sp, OpenedModtype (dir,_)) :: _ -> dir
     | (sp, CompilingLibrary dir) :: _ -> dir
     | _::l -> recalc l
@@ -231,13 +231,13 @@ let export_segment seg =
     clean [] seg
 
 
-let start_module id mp nametab = 
+let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
   let prefix = dir,(mp,empty_dirpath) in
   let oname = make_path id, make_kn id in
   if Nametab.exists_module dir then
     errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
-  add_entry oname (OpenedModule (prefix,nametab));
+  add_entry oname (OpenedModule (export,prefix,nametab));
   path_prefix := prefix;
   prefix
 (*  add_frozen_state () must be called in declaremods *)
@@ -245,7 +245,7 @@ let start_module id mp nametab =
 let end_module id = 
   let oname,nametab = 
     try match find_entry_p is_something_opened with
-      | oname,OpenedModule (_,nametab) -> 
+      | oname,OpenedModule (_,_,nametab) -> 
 	  let sp = fst oname in
 	  let id' = basename sp in
 	  if id<>id' then error "this is not the last opened module"; 
diff --git a/library/lib.mli b/library/lib.mli
index 4411bcbb63..c43155816c 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -24,7 +24,7 @@ open Mod_subst
 type node = 
   | Leaf of obj
   | CompilingLibrary of object_prefix
-  | OpenedModule of object_prefix * Summary.frozen
+  | OpenedModule of bool option * object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
   | ClosedSection of bool * dir_path * library_segment
@@ -101,7 +101,7 @@ val what_is_opened : unit -> object_name * node
 (*s Modules and module types *)
 
 val start_module : 
-  module_ident -> module_path -> Summary.frozen -> object_prefix
+  bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_module : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment