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

4 files changed, 45 insertions, 28 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 041e32bf6..049745ca9 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -80,6 +80,16 @@ let lookup_modtype (loc,qid) =
     | Not_found ->
 	Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
 
+let lookup_module_or_modtype (loc,qid) =
+  try
+    let mp = Nametab.locate_module qid in
+    Dumpglob.dump_modref loc mp "modtype"; (mp,true)
+  with Not_found -> try
+    let mp = Nametab.locate_modtype qid in
+    Dumpglob.dump_modref loc mp "mod"; (mp,false)
+  with Not_found ->
+    Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid)
+
 let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       With_Module (fqid,lookup_module qid)
@@ -87,22 +97,38 @@ let transl_with_decl env = function
       With_Definition (fqid,interp_constr Evd.empty env c)
 
 let rec interp_modexpr env = function
-  | CMEident qid ->
+  | CMident qid ->
       MSEident (lookup_module qid)
-  | CMEapply (me1,me2) ->
+  | CMapply (me1,me2) ->
       let me1 = interp_modexpr env me1 in
       let me2 = interp_modexpr env me2 in
 	MSEapply(me1,me2)
+  | CMwith _ -> Modops.error_with_in_module ()
+
 
 let rec interp_modtype env = function
-  | CMTEident qid ->
+  | CMident qid ->
       MSEident (lookup_modtype qid)
-  | CMTEapply (mty1,me) ->
+  | CMapply (mty1,me) ->
       let mty' = interp_modtype env mty1 in
       let me' = interp_modexpr env me in
 	MSEapply(mty',me')
-  | CMTEwith (mty,decl) ->
+  | CMwith (mty,decl) ->
       let mty = interp_modtype env mty in
       let decl = transl_with_decl env decl in
 	MSEwith(mty,decl)
 
+let rec interp_modexpr_or_modtype env = function
+  | CMident qid ->
+      let (mp,ismod) = lookup_module_or_modtype qid in
+      (MSEident mp, ismod)
+  | CMapply (me1,me2) ->
+      let me1,ismod1 = interp_modexpr_or_modtype env me1 in
+      let me2,ismod2 = interp_modexpr_or_modtype env me2 in
+      if not ismod2 then Modops.error_application_to_module_type ();
+      (MSEapply (me1,me2), ismod1)
+  | CMwith (me,decl) ->
+      let me,ismod = interp_modexpr_or_modtype env me in
+      let decl = transl_with_decl env decl in
+      if ismod then Modops.error_with_in_module ();
+      (MSEwith(me,decl), ismod)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index f39205d8b..e528b7af7 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -21,8 +21,15 @@ open Topconstr
 (* Module expressions and module types are interpreted relatively to
    eventual functor or funsig arguments. *)
 
-val interp_modtype : env -> module_type_ast -> module_struct_entry
+val interp_modtype : env -> module_ast -> module_struct_entry
 
 val interp_modexpr : env -> module_ast -> module_struct_entry
 
+(* The following function tries to interprete an ast as a module,
+   and in case of failure, interpretes this ast as a module type.
+   The boolean is true for a module, false for a module type *)
+
+val interp_modexpr_or_modtype : env -> module_ast ->
+ module_struct_entry * bool
+
 val lookup_module : qualid located -> module_path
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 155fd1c02..d93e1ab14 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1005,17 +1005,9 @@ type with_declaration_ast =
   | CWith_Definition of identifier list located * constr_expr
 
 type module_ast =
-  | CMEident of qualid located
-  | CMEapply of module_ast * module_ast
-
-type module_type_ast =
-  | CMTEident of qualid located
-  | CMTEapply of module_type_ast * module_ast
-  | CMTEwith of module_type_ast * with_declaration_ast
-
-type include_ast =
-  | CIMTE of module_type_ast list
-  | CIME of module_ast list
+  | CMident of qualid located
+  | CMapply of module_ast * module_ast
+  | CMwith of module_ast * with_declaration_ast
 
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6e3951b2f..1b1698f95 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -242,17 +242,9 @@ type with_declaration_ast =
   | CWith_Definition of identifier list located * constr_expr
 
 type module_ast =
-  | CMEident of qualid located
-  | CMEapply of module_ast * module_ast
-
-type module_type_ast =
-  | CMTEident of qualid located
-  | CMTEapply of module_type_ast * module_ast
-  | CMTEwith of module_type_ast * with_declaration_ast
-
-type include_ast =
-  | CIMTE of module_type_ast list
-  | CIME of module_ast list
+  | CMident of qualid located
+  | CMapply of module_ast * module_ast
+  | CMwith of module_ast * with_declaration_ast
 
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)