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

2 files changed, 29 insertions, 28 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 97047ebd7..5db0e0abc 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -897,9 +897,8 @@ let get_includeself_substobjs env objs me is_mod =
     ([],mp_self,subst_objects subst objects)
   with NothingToDo -> objs
 
-let declare_one_include interp_struct me_ast is_mod =
+let declare_one_include_inner (me,is_mod) =
   let env = Global.env() in
-  let me = interp_struct env me_ast in
   let mp1,_ = current_prefix () in
   let (mbids,mp,objs)=
     if is_mod then
@@ -918,11 +917,11 @@ let declare_one_include interp_struct me_ast is_mod =
   ignore (add_leaf id
 	    (in_include ((me,is_mod), substobjs)))
 
+let declare_one_include interp_struct me_ast =
+  declare_one_include_inner (interp_struct (Global.env()) me_ast)
 
-let declare_include_ interp_struct me_asts is_mod =
-  List.iter
-    (fun me -> declare_one_include interp_struct me is_mod)
-    me_asts
+let declare_include_ interp_struct me_asts =
+  List.iter (declare_one_include interp_struct) me_asts
 
 (** Versions of earlier functions taking care of the freeze/unfreeze
     of summaries *)
@@ -934,17 +933,17 @@ let protect_summaries f =
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
 
-let declare_include interp_struct me_asts is_mod =
+let declare_include interp_struct me_asts =
   protect_summaries
-    (fun _ -> declare_include_ interp_struct me_asts is_mod)
+    (fun _ -> declare_include_ interp_struct me_asts)
 
-let declare_modtype interp_mt id args mtys mty_l =
+let declare_modtype interp_mt interp_mix id args mtys mty_l =
   let declare_mt fs = match mty_l with
     | [] -> assert false
     | [mty] -> declare_modtype_ interp_mt id args mtys mty fs
     | mty_l ->
 	ignore (start_modtype_ interp_mt id args mtys fs);
-	declare_include_ interp_mt mty_l false;
+	declare_include_ interp_mix mty_l;
 	end_modtype ()
   in
   protect_summaries declare_mt
@@ -952,13 +951,13 @@ let declare_modtype interp_mt id args mtys mty_l =
 let start_modtype interp_modtype id args mtys =
   protect_summaries (start_modtype_ interp_modtype id args mtys)
 
-let declare_module interp_mt interp_me id args mtys me_l =
+let declare_module interp_mt interp_me interp_mix id args mtys me_l =
   let declare_me fs = match me_l with
     | [] -> declare_module_ interp_mt interp_me id args mtys None fs
     | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs
     | me_l ->
 	ignore (start_module_ interp_mt None id args mtys fs);
-	declare_include_ interp_me me_l true;
+	declare_include_ interp_mix me_l;
 	end_module ()
   in
   protect_summaries declare_me
diff --git a/library/declaremods.mli b/library/declaremods.mli
index ae0b0aa10..1db3d95a8 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -37,16 +37,17 @@ open Lib
 *)
 
 val declare_module :
-  (env -> 'modtype -> module_struct_entry) ->
-  (env -> 'modexpr -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry * bool) ->
   identifier ->
-  (identifier located list * 'modtype) list ->
-  'modtype Topconstr.module_signature ->
-  'modexpr list -> module_path
+  (identifier located list * 'modast) list ->
+  'modast Topconstr.module_signature ->
+  'modast list -> module_path
 
-val start_module : (env -> 'modtype -> module_struct_entry) ->
-  bool option -> identifier -> (identifier located list * 'modtype) list ->
-  'modtype Topconstr.module_signature -> module_path
+val start_module : (env -> 'modast -> module_struct_entry) ->
+  bool option -> identifier -> (identifier located list * 'modast) list ->
+  'modast Topconstr.module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -54,13 +55,14 @@ val end_module : unit -> module_path
 
 (*s Module types *)
 
-val declare_modtype : (env -> 'modtype -> module_struct_entry) ->
-  identifier -> (identifier located list * 'modtype) list ->
-  'modtype list -> 'modtype list -> module_path
+val declare_modtype : (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry * bool) ->
+  identifier -> (identifier located list * 'modast) list ->
+  'modast list -> 'modast list -> module_path
 
-val start_modtype : (env -> 'modtype -> module_struct_entry) ->
-  identifier -> (identifier located list * 'modtype) list ->
-  'modtype list -> module_path
+val start_modtype : (env -> 'modast -> module_struct_entry) ->
+  identifier -> (identifier located list * 'modast) list ->
+  'modast list -> module_path
 
 val end_modtype : unit -> module_path
 
@@ -103,8 +105,8 @@ val import_module : bool -> module_path -> unit
 
 (* Include  *)
 
-val declare_include : (env -> 'struct_expr -> module_struct_entry) ->
-  'struct_expr list -> bool -> unit
+val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
+  'struct_expr list -> unit
 
 (*s [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented