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, 35 insertions, 27 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3a99b24738..38ab689f55 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -389,13 +389,13 @@ GEXTEND Gram
     [ [ (* Interactive module declaration *)
         IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; mty_o = OPT of_module_type;
-	mexpr_o = OPT is_module_expr ->
-	  VernacDefineModule (export, id, bl, mty_o, mexpr_o)
-
+	o = OPT is_module_expr ->
+	  VernacDefineModule (export, id, bl, mty_o,
+			      match o with None -> [] | Some l -> l)
       | IDENT "Module"; "Type"; id = identref;
-	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
-	  VernacDeclareModuleType (id, bl, mty_o)
-
+	bl = LIST0 module_binder; o = OPT is_module_type ->
+	  VernacDeclareModuleType (id, bl,
+				   match o with None -> [] | Some l -> l)
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; ":"; mty = module_type ->
 	  VernacDeclareModule (export, id, bl, (mty,true))
@@ -413,28 +413,35 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr))
-      | IDENT "Include"; "Type"; expr = module_type ->
-          VernacInclude(false,CIMTE(expr))
-      | IDENT "Include"; "Self"; expr = module_expr ->
-          VernacInclude(true,CIME(expr))
-      | IDENT "Include"; "Self"; "Type"; expr = module_type ->
-          VernacInclude(true,CIMTE(expr)) ] ]
+      | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr ->
+	  VernacInclude(false,CIME(e,l))
+      | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type ->
+          VernacInclude(false,CIMTE(e,l))
+      | IDENT "Include"; "Self"; e = module_expr ->
+          VernacInclude(true,CIME(e,[]))
+      | IDENT "Include"; "Self"; "Type"; e = module_type ->
+          VernacInclude(true,CIMTE(e,[])) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
       | IDENT "Export" -> Some true
       |  -> None ] ]
   ;
+  ext_module_type:
+    [ [ "<+"; mty = module_type -> mty ] ]
+  ;
+  ext_module_expr:
+    [ [ "<+"; mexpr = module_expr -> mexpr ] ]
+  ;
   of_module_type:
     [ [ ":"; mty = module_type -> (mty, true)
       | "<:"; mty = module_type -> (mty, false) ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type -> mty ] ]
+    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr -> mexpr ] ]
+    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ]
   ;
 
   (* Module binder  *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 52ef1875f4..4407ca6aa4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -751,7 +751,8 @@ let rec pr_vernac = function
       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)
+	       (if bd = [] then mt () else str ":= ") ++
+	       prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd)
   | VernacDeclareModule (export,id,bl,m1) ->
       let b = pr_module_binders_list bl pr_lconstr in
 	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
@@ -760,17 +761,17 @@ let rec pr_vernac = function
   | VernacDeclareModuleType (id,bl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
-		 pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
-  | VernacInclude (b,in_ast) ->
-      begin
-	match in_ast with
-	  | CIMTE mty ->
-	      hov 2 (str"Include " ++ str (if b then "Self " else "") ++
-		     pr_module_type pr_lconstr mty)
-	  | CIME mexpr ->
-	      hov 2 (str"Include " ++ str (if b then "Self " else "") ++
-		     pr_module_expr mexpr)
-      end
+		 (if m = [] then mt () else str ":= ") ++
+		 prlist_with_sep (fun () -> str " <+ ")
+		                 (pr_module_type pr_lconstr) m)
+  | VernacInclude (b,CIMTE(mty,mtys)) ->
+      let pr_mty = pr_module_type pr_lconstr in
+      hov 2 (str"Include " ++ str (if b then "Self " else "") ++ str "Type " ++
+	     prlist_with_sep (fun () -> str " <+ ") pr_mty (mty::mtys))
+  | VernacInclude (b,CIME(mexpr,mexprs)) ->
+      let pr_me = pr_module_expr in
+      hov 2 (str"Include " ++ str (if b then "Self " else "") ++
+	     prlist_with_sep (fun () -> str " <+ ") pr_me (mexpr::mexprs))
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++