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

1 files changed, 13 insertions, 12 deletions

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 52ef1875f..4407ca6aa 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 ": ") ++