New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))

 "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
 "Module M (...). Include M1. Include M2. Include M3... End M."

 Moreover M2,M3,etc can be functors as long as they find what they need in what
 comes before them (see new command "Include Self").
 The only real constraint is that M1,M2,M3,... should not have common elements
 (for the moment (?)).

 Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.

 Note that this <+ is _not_ a primitive construct of the module language,
 for instance it cannot be used in signature (Module M <: M1 <+ M2 is
 illegal for the moment).

 Some example of use in Decidable2 and NZAxioms

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

2 files changed, 21 insertions, 21 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2008e5f01f..76e7eb0b80 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -460,19 +460,19 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
      else (idl,ty)) binders_ast in
   let mp = Declaremods.declare_module
     Modintern.interp_modtype Modintern.interp_modexpr
-    id binders_ast (Some mty_ast_o) None
+    id binders_ast (Some mty_ast_o) []
   in
     Dumpglob.dump_moddef loc mp "mod";
     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 (loc, id) binders_ast mty_ast_o mexpr_ast_o =
+let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* 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.";
-  match mexpr_ast_o with
-    | None ->
+  match mexpr_ast_l with
+    | [] ->
        check_no_pending_proofs ();
        let binders_ast,argsexport =
         List.fold_right
@@ -490,7 +490,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
              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
@@ -500,7 +500,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
           else (idl,ty)) binders_ast in
        let mp =	Declaremods.declare_module
 	  Modintern.interp_modtype Modintern.interp_modexpr
-	  id binders_ast mty_ast_o mexpr_ast_o
+	  id binders_ast mty_ast_o mexpr_ast_l
        in
 	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message
@@ -514,12 +514,12 @@ let vernac_end_module export (loc,id as lid) =
   if_verbose message ("Module "^ string_of_id id ^" is defined") ;
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
-let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
+let vernac_declare_module_type (loc,id) binders_ast mty_ast_l =
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections.";
 
-  match mty_ast_o with
-    | None ->
+  match mty_ast_l with
+    | [] ->
        check_no_pending_proofs ();
        let binders_ast,argsexport =
         List.fold_right
@@ -536,7 +536,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
             (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
@@ -545,7 +545,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
 			"and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype
-	  id binders_ast base_mty in
+	  id binders_ast mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message
 	    ("Module Type "^ string_of_id id ^" is defined")
@@ -556,12 +556,12 @@ let vernac_end_modtype (loc,id) =
   if_verbose message ("Module Type "^ string_of_id id ^" is defined")
 
 let vernac_include is_self = function
-  | CIMTE mty_ast ->
+  | CIMTE (mty,mtys) ->
       Declaremods.declare_include
-	Modintern.interp_modtype mty_ast false is_self
-  | CIME mexpr_ast ->
+	Modintern.interp_modtype mty mtys false is_self
+  | CIME (mexpr, mexprs) ->
       Declaremods.declare_include
-	Modintern.interp_modexpr mexpr_ast true is_self
+	Modintern.interp_modexpr mexpr mexprs true is_self
 
 (**********************)
 (* Gallina extensions *)
@@ -1329,12 +1329,12 @@ let interp c = match c with
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
       vernac_declare_module export lid bl mtyo
-  | VernacDefineModule (export,lid,bl,mtyo,mexpro) ->
-      vernac_define_module export lid bl mtyo mexpro
+  | VernacDefineModule (export,lid,bl,mtyo,mexprl) ->
+      vernac_define_module export lid bl mtyo mexprl
   | VernacDeclareModuleType (lid,bl,mtyo) ->
       vernac_declare_module_type lid bl mtyo
-  | VernacInclude (is_self,in_ast) ->
-      vernac_include is_self in_ast
+  | VernacInclude (is_self,in_asts) ->
+      vernac_include is_self in_asts
   (* Gallina extensions *)
   | VernacBeginSection lid -> vernac_begin_section lid
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 366308bfa6..ccb850651b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -261,9 +261,9 @@ type vernac_expr =
   | 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
+      module_binder list * (module_type_ast * bool) option * module_ast list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_type_ast option
+      module_binder list * module_type_ast list
   | VernacInclude of bool * include_ast
 
   (* Solving *)