- 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

13 files changed, 151 insertions, 167 deletions

diff --git a/CHANGES b/CHANGES
index 97bb4fc8d1..098ab23ffd 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
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e9e4a15605..ea1484d002 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1517,7 +1517,7 @@ let rec xlate_module_type = function
 
 let xlate_module_binder_list (l:module_binder list) =
   CT_module_binder_list
-    (List.map (fun (idl, mty) ->
+    (List.map (fun (_, idl, mty) ->
 		 let idl1 = 
 		   List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
 		 let fst,idl2 = match idl1 with
@@ -1915,20 +1915,18 @@ let rec xlate_vernac =
 			    | Some mty1 ->
 				CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
 				  (xlate_module_type mty1))
-   | VernacDefineModule((_, id), bl, mty_o, mexpr_o) ->
+   | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
        CT_module(xlate_ident id, 
 		 xlate_module_binder_list bl,
 		 xlate_module_type_check_opt mty_o,
 		 match mexpr_o with
 		     None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
 		   | Some m -> xlate_module_expr m)
-  | VernacDeclareModule((_, id), bl, mty_o, mexpr_o) -> 
+  | VernacDeclareModule(_,(_, id), bl, mty_o) -> 
        CT_declare_module(xlate_ident id, 
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt mty_o,
-		 match mexpr_o with
-		     None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
-		   | Some m -> xlate_module_expr m)
+		 xlate_module_type_check_opt (Some mty_o),
+		 CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
    | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in
       CT_require (ct_impexp, ct_spec, 
diff --git a/ide/coq.ml b/ide/coq.ml
index b171aab6b7..0a72c97bc4 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -329,8 +329,8 @@ type reset_info = NoReset | Reset of Names.identifier * bool ref
 let compute_reset_info = function 
   | VernacDefinition (_, (_,id), DefineBody _, _) 
   | VernacBeginSection (_,id) 
-  | VernacDefineModule ((_,id), _, _, _) 
-  | VernacDeclareModule ((_,id), _, _, _)
+  | VernacDefineModule (_,(_,id), _, _, _) 
+  | VernacDeclareModule (_,(_,id), _, _)
   | VernacDeclareModuleType ((_,id), _, _)
   | VernacAssumption (_, (_,((_,id)::_,_))::_)
   | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 11af7ada6b..bd06c0b07d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -518,8 +518,8 @@ let update_on_end_of_proof id =
 let update_on_end_of_segment id =
   let lookup_section = function 
     | { ast = _, ( VernacBeginSection id'
-		 | VernacDefineModule (id',_,_,None)
-		 | VernacDeclareModule (id',_,_,None)
+		 | VernacDefineModule (_,id',_,_,None)
+		 | VernacDeclareModule (_,id',_,_)
 		 | VernacDeclareModuleType (id',_,None)); 
 	reset_info = Reset (_, r) } 
        when id = id' -> raise Exit
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
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d09e167b15..26a38e381e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -348,9 +348,14 @@ GEXTEND Gram
 	IDENT "Section"; id = identref -> VernacBeginSection id
       | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ]
   ;
+  export_token:
+    [ [ IDENT "Import" -> Some false
+      | IDENT "Export" -> Some true
+      |  -> None ] ]
+  ;
   module_vardecls:
-    [ [ id = identref; idl = ident_comma_list_tail; ":";
-        mty = Module.module_type -> (id::idl,mty) ] ]
+    [ [ export = export_token; id = identref; idl = ident_comma_list_tail; ":";
+        mty = Module.module_type -> (export,id::idl,mty) ] ]
   ;
   module_binders:
     [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ]
@@ -371,19 +376,18 @@ GEXTEND Gram
   gallina_ext:
     [ [ 
 	  (* Interactive module declaration *)
-	IDENT "Module"; id = identref; 
+	IDENT "Module"; export = export_token; id = identref; 
 	bl = module_binders_list; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
-	  VernacDefineModule (id, bl, mty_o, mexpr_o)
+	  VernacDefineModule (export, id, bl, mty_o, mexpr_o)
 	  
       | IDENT "Module"; "Type"; id = identref; 
 	bl = module_binders_list; mty_o = OPT is_module_type ->
 	  VernacDeclareModuleType (id, bl, mty_o)
 	  
-      | IDENT "Declare"; IDENT "Module"; id = identref; 
-	bl = module_binders_list; mty_o = OPT of_module_type; 
-	mexpr_o = OPT is_module_expr ->
-	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
+      | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; 
+	bl = module_binders_list; mty_o = of_module_type ->
+	  VernacDeclareModule (export, id, bl, mty_o)
 
 	  (* This end a Section a Module or a Module Type *)
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 2d595088ca..acc691082c 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -307,19 +307,18 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
-	IDENT "Module"; id = identref; 
+        IDENT "Module"; export = export_token; id = identref; 
 	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
-	  VernacDefineModule (id, bl, mty_o, mexpr_o)
+	  VernacDefineModule (export, id, bl, mty_o, mexpr_o)
 	  
       | IDENT "Module"; "Type"; id = identref; 
 	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
 	  VernacDeclareModuleType (id, bl, mty_o)
 	  
-      | IDENT "Declare"; IDENT "Module"; id = identref; 
-	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
-	mexpr_o = OPT is_module_expr ->
-	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
+      | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; 
+	bl = LIST0 module_binder; mty_o = of_module_type ->
+	  VernacDeclareModule (export, id, bl, mty_o)
       (* Section beginning *)
       | IDENT "Section"; id = identref -> VernacBeginSection id
       | IDENT "Chapter"; id = identref -> VernacBeginSection id
@@ -360,8 +359,8 @@ GEXTEND Gram
 
   (* Module binder  *)
   module_binder:
-    [ [ "("; idl = LIST1 identref; ":"; mty = module_type; ")" ->
-          (idl,mty) ] ]
+    [ [ "("; export = export_token; idl = LIST1 identref; ":";
+         mty = module_type; ")" -> (export,idl,mty) ] ]
   ;
 
   (* Module expressions *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f8ce873d1b..36d85ddca7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -325,107 +325,86 @@ let vernac_scheme = build_scheme
 (**********************)
 (* Modules            *)
 
-let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = 
+let vernac_import export refl =
+  let import_one ref = 
+    let qid = qualid_of_reference ref in
+      Library.import_library export qid
+  in
+    List.iter import_one refl;
+    Lib.add_frozen_state ()
+
+(*  else
+    let import (loc,qid) = 
+      try
+	let mp = Nametab.locate_module qid in
+	  Declaremods.import_module mp
+      with Not_found ->
+	user_err_loc
+        (loc,"vernac_import",
+	 str ((string_of_qualid qid)^" is not a module"))
+    in
+      List.iter import qidl;
+*)
+
+let vernac_declare_module export id binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
-
-  if not (Lib.is_modtype ()) then
-    error "Declare Module allowed in module types only";
-
-  let constrain_mty = match mty_ast_o with
-      Some (_,true) -> true
-    | _ -> false
-  in
-
-  match mty_ast_o, constrain_mty, mexpr_ast_o with
-    | _, false, None ->  (* no ident, no/soft type *)
-	Declaremods.start_module Modintern.interp_modtype
-	  id binders_ast mty_ast_o;
-	if_verbose message 
-	  ("Interactive Declaration of Module "^ string_of_id id ^" started")
-	  
-    | Some _, true, None           (* no ident, hard type *)
-    | _, false, Some (CMEident _) ->  (* ident, no/soft type *)
-	Declaremods.declare_module 
-	  Modintern.interp_modtype Modintern.interp_modexpr
-	  id binders_ast mty_ast_o mexpr_ast_o;
-	if_verbose message 
-	  ("Module "^ string_of_id id ^" is declared")
-
-    | _, true, Some (CMEident _) -> (* ident, hard type *)
-	error "You cannot declare an equality and a type in module declaration"
-
-    | _, _, Some _ ->    (* not ident *)
-	error "Only simple modules allowed in module declarations"
-
-    | None,true,None -> assert false  (* 1st None ==> false *)
-
-let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o = 
+  let binders_ast = List.map
+   (fun (export,idl,ty) ->
+     if export <> None then
+      error ("Arguments of a functor declaration cannot be exported. " ^
+       "Remove the \"Export\" and \"Import\" keywords from every functor " ^
+       "argument.")
+     else (idl,ty)) binders_ast in
+  Declaremods.declare_module 
+    Modintern.interp_modtype Modintern.interp_modexpr
+     id binders_ast (Some mty_ast_o) None;
+  if_verbose message ("Module "^ string_of_id id ^" is declared");
+  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+
+let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
- 
-  if Lib.is_modtype () then
-    error "Module definitions not allowed in module types. Use Declare Module instead";
-
   match mexpr_ast_o with
     | None ->
-	Declaremods.start_module Modintern.interp_modtype
+       let binders_ast,argsexport =
+        List.fold_right
+         (fun (export,idl,ty) (args,argsexport) ->
+           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+             ([],[]) in
+	Declaremods.start_module Modintern.interp_modtype export
 	  id binders_ast mty_ast_o;
 	if_verbose message 
-	  ("Interactive Module "^ string_of_id id ^" started")
-	  
+	  ("Interactive Module "^ string_of_id id ^" started") ;
+        List.iter
+         (fun (export,id) ->
+           option_iter
+            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+         ) argsexport
     | Some _ ->
+       let binders_ast = List.map
+        (fun (export,idl,ty) ->
+          if export <> None then
+           error ("Arguments of a functor definition can be imported only if" ^
+                  " the definition is interactive. Remove the \"Export\" and " ^
+                  "\"Import\" keywords from every functor argument.")
+          else (idl,ty)) binders_ast in
 	Declaremods.declare_module 
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o;
 	if_verbose message 
-	  ("Module "^ string_of_id id ^" is defined")
+	  ("Module "^ string_of_id id ^" is defined");
+        option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+         export
 
-(* let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =  *)
-(*   (\* We check the state of the system (in section, in module type) *)
-(*      and what module information is supplied *\) *)
-(*   if Lib.sections_are_opened () then *)
-(*     error "Modules and Module Types are not allowed inside sections"; *)
- 
-(*   let constrain_mty = match mty_ast_o with *)
-(*       Some (_,true) -> true *)
-(*     | _ -> false *)
-(*   in *)
-
-(*   match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *)
-(*     | _, None, _, None  *)
-(*     | true, Some _, false, None *)
-(*     | false, _, _, None -> *)
-(* 	Declaremods.start_module Modintern.interp_modtype *)
-(* 	  id binders_ast mty_ast_o; *)
-(* 	if_verbose message  *)
-(* 	  ("Interactive Module "^ string_of_id id ^" started") *)
-	  
-(*     | true, Some _, true, None *)
-(*     | true, _, false, Some (CMEident _) *)
-(*     | false, _, _, Some _ -> *)
-(* 	Declaremods.declare_module  *)
-(* 	  Modintern.interp_modtype Modintern.interp_modexpr *)
-(* 	  id binders_ast mty_ast_o mexpr_ast_o; *)
-(* 	if_verbose message  *)
-(* 	  ("Module "^ string_of_id id ^" is defined") *)
-
-(*     | true, _, _, _ -> *)
-(* 	error "Module definition not allowed in a Module Type" *)
-
-let vernac_end_module id =
+let vernac_end_module export id =
   Declaremods.end_module id;
-  if_verbose message 
-    (if Lib.is_modtype () then 
-       "Module "^ string_of_id id ^" is declared"
-     else
-       "Module "^ string_of_id id ^" is defined")
-
-  
+  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 
 let vernac_declare_module_type id binders_ast mty_ast_o =
@@ -434,11 +413,28 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
   
   match mty_ast_o with
     | None ->
+       let binders_ast,argsexport =
+        List.fold_right
+         (fun (export,idl,ty) (args,argsexport) ->
+           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+             ([],[]) in
 	Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
 	if_verbose message 
-	  ("Interactive Module Type "^ string_of_id id ^" started")
+	  ("Interactive Module Type "^ string_of_id id ^" started");
+        List.iter
+         (fun (export,id) ->
+           option_iter
+            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+         ) argsexport
 	  
     | Some base_mty ->
+       let binders_ast = List.map
+        (fun (export,idl,ty) ->
+          if export <> None then
+           error ("Arguments of a functor definition can be imported only if" ^
+                  " the definition is interactive. Remove the \"Export\" " ^
+                  "and \"Import\" keywords from every functor argument.")
+          else (idl,ty)) binders_ast in
 	Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty;
 	if_verbose message 
@@ -480,7 +476,7 @@ let vernac_end_segment id =
   check_no_pending_proofs ();
   try
     match Lib.what_is_opened () with
-      | _,Lib.OpenedModule _ -> vernac_end_module id
+      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
       | _,Lib.OpenedModtype _ -> vernac_end_modtype id
       | _,Lib.OpenedSection _ -> vernac_end_section id
       | _ -> anomaly "No more opened things"
@@ -527,26 +523,6 @@ let vernac_require import _ qidl =
       (if not !Options.v7 then List.iter test_renamed_module qidl;
        raise e)
       
-let vernac_import export refl =
-  let import_one ref = 
-    let qid = qualid_of_reference ref in
-      Library.import_library export qid
-  in
-    List.iter import_one refl;
-    Lib.add_frozen_state ()
-
-(*  else
-    let import (loc,qid) = 
-      try
-	let mp = Nametab.locate_module qid in
-	  Declaremods.import_module mp
-      with Not_found ->
-	user_err_loc
-        (loc,"vernac_import",
-	 str ((string_of_qualid qid)^" is not a module"))
-    in
-      List.iter import qidl;
-*)
 
 let vernac_canonical locqid =
   Recordobj.objdef_declare (Nametab.global locqid)
@@ -1207,10 +1183,10 @@ let interp c = match c with
   | VernacScheme l -> vernac_scheme l
 
   (* Modules *)
-  | VernacDeclareModule ((_,id),bl,mtyo,mexpro) -> 
-      vernac_declare_module id bl mtyo mexpro
-  | VernacDefineModule ((_,id),bl,mtyo,mexpro) -> 
-      vernac_define_module id bl mtyo mexpro
+  | VernacDeclareModule (export,(_,id),bl,mtyo) -> 
+      vernac_declare_module export id bl mtyo
+  | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> 
+      vernac_define_module export id bl mtyo mexpro
   | VernacDeclareModuleType ((_,id),bl,mtyo) -> 
       vernac_declare_module_type id bl mtyo
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index afcc361f83..b5e7faa606 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -155,7 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type module_binder = lident list * module_type_ast
+type module_binder = bool option * lident list * module_type_ast
 
 type proof_end =
   | Admitted
@@ -217,9 +217,9 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
 
   (* Modules and Module Types *)
-  | VernacDeclareModule of lident * 
-      module_binder list * (module_type_ast * bool) option * module_ast option
-  | VernacDefineModule of lident * 
+  | VernacDeclareModule of bool option * lident * 
+      module_binder list * (module_type_ast * bool)
+  | VernacDefineModule of bool option * lident * 
       module_binder list * (module_type_ast * bool) option * module_ast option
   | VernacDeclareModuleType of lident * 
       module_binder list * module_type_ast option
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index e16e59d0ef..4b47b8d0aa 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -245,7 +245,12 @@ let pr_of_module_type prc (mty,b) =
   str (if b then ":" else "<:") ++
   pr_module_type prc mty
 
-let pr_module_vardecls pr_c (idl,mty) =
+let pr_require_token = function
+  | Some true -> str "Export "
+  | Some false -> str "Import "
+  | None -> mt()
+
+let pr_module_vardecls pr_c (export,idl,mty) =
   let m = pr_module_type pr_c mty in
   (* Update the Nametab for interpreting the body of module/modtype *)
   let lib_dir = Lib.library_dp() in
@@ -255,7 +260,8 @@ let pr_module_vardecls pr_c (idl,mty) =
        Modintern.interp_modtype (Global.env()) mty]) idl;
   (* Builds the stream *)
   spc() ++
-  hov 1 (str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+  hov 1 (str"(" ++ pr_require_token export ++
+   prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
 
 let pr_module_binders l pr_c = 
   (* Effet de bord complexe pour garantir la declaration des noms des
@@ -362,11 +368,6 @@ let pr_thm_token = function
   | Fact -> str"Fact"
   | Remark -> str"Remark"
 
-let pr_require_token = function
-  | Some true -> str " Export"
-  | Some false -> str " Import"
-  | None -> mt()
-
 let pr_syntax_modifier = function
   | SetItemLevel (l,NextLevel) ->
       prlist_with_sep sep_v2 str l ++
@@ -842,7 +843,7 @@ let rec pr_vernac = function
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2
-      (str "Require" ++ pr_require_token exp ++ spc() ++
+      (str "Require" ++ spc() ++ pr_require_token exp ++
       (match spe with
       |	None -> mt()
       |	Some flag ->
@@ -867,16 +868,17 @@ let rec pr_vernac = function
 	spc() ++ pr_class_rawexpr c2)
 
   (* Modules and Module Types *)
-  | VernacDefineModule (m,bl,ty,bd) ->
+  | VernacDefineModule (export,m,bl,ty,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Module " ++ pr_lident m ++ b ++
+      hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
+             pr_lident m ++ b ++
              pr_opt (pr_of_module_type pr_lconstr) ty ++
              pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
-  | VernacDeclareModule (id,bl,m1,m2) ->
+  | VernacDeclareModule (export,id,bl,m1) ->
       let b = pr_module_binders_list bl pr_lconstr in 
-      hov 2 (str"Declare Module " ++ pr_lident id ++ b ++
-             pr_opt (pr_of_module_type pr_lconstr) m1 ++
-             pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
+      hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
+             pr_lident id ++ b ++
+             pr_of_module_type pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in 
       hov 2 (str"Module Type " ++ pr_lident id ++ b ++
@@ -898,7 +900,7 @@ let rec pr_vernac = function
 
   (* Auxiliary file and library management *)
   | VernacRequireFrom (exp,spe,f) -> hov 2
-      (str"Require " ++ pr_require_token exp ++ spc() ++
+      (str"Require" ++ spc() ++ pr_require_token exp ++
       (match spe with
         | None -> mt()
         | Some false -> str"Implementation" ++ spc()
@@ -1111,7 +1113,7 @@ let pr_vernac = function
       (* Renamed modules *)
       List.mem (string_of_id r) ["zarith_aux";"fast_integer"] ->
       warning ("Replacing obsolete module "^(string_of_id r)^" with ZArith");
-	(str "Require" ++ pr_require_token exp ++ spc() ++
+	(str "Require" ++ spc() ++ pr_require_token exp ++
 	(match spe with
 	  | None -> mt()
 	  | Some flag ->