Include can accept both Module and Module Type

 Syntax Include Type is still active, but deprecated, and triggers a warning.
 The syntax M <+ M' <+ M'', which performs internally an Include, also
 benefits from this: M, M', M'' can be independantly modules or module type.

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

3 files changed, 28 insertions, 37 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4672a732a..f4d588b57 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -397,9 +397,10 @@ GEXTEND Gram
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
       | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr ->
-	  VernacInclude(CIME(e::l))
+	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type ->
-          VernacInclude(CIMTE(e::l)) ] ]
+	  warning "Include Type is deprecated; use Include instead";
+          VernacInclude(e::l) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
@@ -440,11 +441,11 @@ GEXTEND Gram
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2)
+      | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2)
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
@@ -454,10 +455,10 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CMTEident qid
+    [ [ qid = qualid -> CMident qid
       | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me)
-      | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
+      | mty = module_type; me = module_expr_atom -> CMapply (mty,me)
+      | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl)
       ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d724e2e73..6d5455b1b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -214,7 +214,7 @@ module Constr :
 module Module :
   sig
     val module_expr : module_ast Gram.Entry.e
-    val module_type : module_type_ast Gram.Entry.e
+    val module_type : module_ast Gram.Entry.e
   end
 
 module Tactic :
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4b1162dbd..92a455abc 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -234,29 +234,22 @@ let pr_with_declaration pr_c = function
       str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
       pr_located pr_qualid qid
 
-let rec pr_module_type pr_c = function
-  | CMTEident qid -> spc () ++ pr_located pr_qualid qid
-  | CMTEwith (mty,decl) ->
-      let m = pr_module_type pr_c mty in
+let rec pr_module_ast pr_c = function
+  | CMident qid -> spc () ++ pr_located pr_qualid qid
+  | CMwith (mty,decl) ->
+      let m = pr_module_ast pr_c mty in
       let p = pr_with_declaration pr_c decl in
       m ++ spc() ++ str"with" ++ spc() ++ p
-  | CMTEapply (fexpr,mexpr)->
-      let f = pr_module_type pr_c fexpr in
-      let m = pr_module_expr mexpr in
-	f ++ spc () ++ m
-
-and  pr_module_expr = function
-  | CMEident qid -> pr_located pr_qualid qid
-  | CMEapply (me1,(CMEident _ as me2)) ->
-      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
-  | CMEapply (me1,me2) ->
-      pr_module_expr me1 ++ spc() ++
-      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
+  | CMapply (me1,(CMident _ as me2)) ->
+      pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2
+  | CMapply (me1,me2) ->
+      pr_module_ast pr_c me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
 
 let pr_of_module_type prc = function
-  | Enforce mty -> str ":" ++ pr_module_type prc mty
+  | Enforce mty -> str ":" ++ pr_module_ast prc mty
   | Check mtys ->
-      prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast prc m) mtys
 
 let pr_require_token = function
   | Some true -> str "Export "
@@ -264,7 +257,7 @@ let pr_require_token = function
   | None -> mt()
 
 let pr_module_vardecls pr_c (export,idl,mty) =
-  let m = pr_module_type pr_c mty in
+  let m = pr_module_ast pr_c mty in
   (* Update the Nametab for interpreting the body of module/modtype *)
   let lib_dir = Lib.library_dp() in
   List.iter (fun (_,id) ->
@@ -751,27 +744,24 @@ let rec pr_vernac = function
                pr_lident m ++ b ++
                pr_of_module_type pr_lconstr tys ++
 	       (if bd = [] then mt () else str ":= ") ++
-	       prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd)
+	       prlist_with_sep (fun () -> str " <+ ")
+	        (pr_module_ast pr_lconstr) 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 ++
              pr_lident id ++ b ++
-             pr_module_type pr_lconstr m1)
+             pr_module_ast pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,tyl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in
-      let pr_mt = pr_module_type pr_lconstr in
+      let pr_mt = pr_module_ast pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
 		 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
 		 (if m = [] then mt () else str ":= ") ++
 		 prlist_with_sep (fun () -> str " <+ ") pr_mt m)
-  | VernacInclude (CIMTE(mtys)) ->
-      let pr_mty = pr_module_type pr_lconstr in
-      hov 2 (str"Include Type " ++
-	     prlist_with_sep (fun () -> str " <+ ") pr_mty mtys)
-  | VernacInclude (CIME(mexprs)) ->
-      let pr_me = pr_module_expr in
+  | VernacInclude (mexprs) ->
+      let pr_m = pr_module_ast pr_lconstr in
       hov 2 (str"Include " ++
-	     prlist_with_sep (fun () -> str " <+ ") pr_me mexprs)
+	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++