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

30 files changed, 164 insertions, 162 deletions

diff --git a/CHANGES b/CHANGES
index fb4e921d1..be8b1404a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,8 @@ Vernacular commands
 - Declaring axiomatic type class instances in Module Type should be now
   done via new command "Declare Instance", while the syntax "Instance"
   now always provides a concrete instance, both in and out of Module Type.
+- Include Type is now deprecated since Include now accept both modules and
+  module types. 
 
 Tools
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 4d213e1f2..40fd6f110 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -65,23 +65,17 @@ This command is used to start an interactive module named {\ident}.
 \subsubsection{Reserved commands inside an interactive module:
 \comindex{Include}}
 \begin{enumerate}
-\item {\tt Include {\modexpr}}
+\item {\tt Include {\module}}
 
- Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr}
+  Includes the content of {\module} in the current interactive
+ module. Here {\module} can be a module expresssion or a module type
+ expression. If {\module} is a high-order module or module type
+ expression then the system tries to instanciate {\module}
  by the current interactive module.
 
-\item {\tt Include Type {\modtype}}
+\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
 
- Includes the content of {\modtype} in the current interactive module type. If  {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype}
- by the current interactive module.
-
-\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} 
-
-is a shortcut for {\tt Include {\modexpr$_1$}}  $\ldots$ {\tt Include {\modexpr$_n$}}
-
-\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} 
-
-is a shortcut for {\tt Include Type {\modtype$_1$}}  $\ldots$ {\tt Include Type {\modtype$_n$}}
+is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
 \end{enumerate}
 \subsection{\tt End {\ident}
 \comindex{End}}
@@ -151,23 +145,13 @@ This command is used to start an interactive module type {\ident}.
 \subsubsection{Reserved commands inside an interactive module type:
 \comindex{Include}\comindex{Inline}}
 \begin{enumerate}
-\item {\tt Include {\modexpr}}
-
- Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr}
- by the current interactive module type.
-
-\item {\tt Include Type {\modtype}}
-
- Includes the content of {\modtype} in the current interactive module type. If {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype}
- by the current interactive module type.
-
-\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} 
+\item {\tt Include {\module}}
 
-is a shortcut for {\tt Include {\modexpr$_1$}}  $\ldots$ {\tt Include {\modexpr$_n$}}
+ Same as {\tt Include} inside a module.
 
-\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} 
+\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
 
-is a shortcut for {\tt Include Type {\modtype$_1$}}  $\ldots$ {\tt Include Type {\modtype$_n$}}
+is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
 
 \item {\tt {\declarationkeyword} Inline {\assums} }
 
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 *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 8c014c1d7..000b2d65e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -61,6 +61,9 @@ let error_not_a_modtype_loc loc s =
 let error_not_a_module_loc loc s = 
   user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
 
+let error_not_a_module_or_modtype_loc loc s =
+  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+
 let error_not_a_module s = error_not_a_module_loc dummy_loc s
 
 let error_not_a_constant l = 
@@ -86,6 +89,9 @@ let error_local_context lo =
 let error_no_such_label_sub l l1 =
   error ("The field "^(string_of_label l)^" is missing in "^l1^".")
 
+let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
+
+let error_application_to_module_type _ = error "Module application to a module type."
 
 let destr_functor env mtb =
   match mtb with
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 44d29ee3e..435c196f9 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -84,6 +84,8 @@ val error_not_a_modtype_loc : loc -> string -> 'a
 
 val error_not_a_module_loc : loc -> string -> 'a
 
+val error_not_a_module_or_modtype_loc : loc -> string -> 'a
+
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : label -> 'a
@@ -96,5 +98,7 @@ val error_local_context : label option -> 'a
 
 val error_no_such_label_sub : label->string->'a
 
+val error_with_in_module : unit -> 'a
 
+val error_application_to_module_type : unit -> 'a
 
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
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 ": ") ++
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index cd51b2aff..e60cca9d9 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -258,7 +258,7 @@ End WSfun.
 
 Module Type WS.
   Declare Module E : DecidableType.
-  Include Type WSfun E.
+  Include WSfun E.
 End WS.
 
 
@@ -266,7 +266,7 @@ End WS.
 (** ** Maps on ordered keys, functorial signature *)
 
 Module Type Sfun (E : OrderedType).
-  Include Type WSfun E.
+  Include WSfun E.
   Section elt.
   Variable elt:Type.
    Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
@@ -284,7 +284,7 @@ End Sfun.
 
 Module Type S.
   Declare Module E : OrderedType.
-  Include Type Sfun E.
+  Include Sfun E.
 End S.
 
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index d94ff7c95..8aede5527 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -275,7 +275,7 @@ End WSfun.
 
 Module Type WS.
   Declare Module E : DecidableType.
-  Include Type WSfun E.
+  Include WSfun E.
 End WS.
 
 
@@ -286,7 +286,7 @@ End WS.
     and some stronger specifications for other functions. *)
 
 Module Type Sfun (E : OrderedType).
-  Include Type WSfun E.
+  Include WSfun E.
 
   Parameter lt : t -> t -> Prop.
   Parameter compare : forall s s' : t, Compare lt eq s s'.
@@ -349,7 +349,7 @@ End Sfun.
 
 Module Type S.
   Declare Module E : OrderedType.
-  Include Type Sfun E.
+  Include Sfun E.
 End S.
 
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index effd5e35a..cb18785e6 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -117,7 +117,7 @@ End HasWOps.
 Module Type WOps (E : DecidableType).
   Definition elt := E.t.
   Parameter t : Type. (** the abstract type of sets *)
-  Include Type HasWOps.
+  Include HasWOps.
 End WOps.
 
 
@@ -128,7 +128,7 @@ End WOps.
 
 Module Type WSetsOn (E : DecidableType).
   (** First, we ask for all the functions *)
-  Include Type WOps E.
+  Include WOps E.
 
   (** Logical predicates *)
   Parameter In : elt -> t -> Prop.
@@ -144,8 +144,8 @@ Module Type WSetsOn (E : DecidableType).
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq : t -> t -> Prop := Equal.
-  Include Type IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
-  Include Type HasEqDec.
+  Include IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
+  Include HasEqDec.
 
   (** Specifications of set operators *)
 
@@ -197,7 +197,7 @@ End WSetsOn.
 
 Module Type WSets.
   Declare Module E : DecidableType.
-  Include Type WSetsOn E.
+  Include WSetsOn E.
 End WSets.
 
 (** ** Functorial signature for sets on ordered elements
@@ -226,7 +226,7 @@ Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.
 
 
 Module Type SetsOn (E : OrderedType).
-  Include Type WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+  Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
 
   Section Spec.
   Variable s s': t.
@@ -266,7 +266,7 @@ End SetsOn.
 
 Module Type Sets.
   Declare Module E : OrderedType.
-  Include Type SetsOn E.
+  Include SetsOn E.
 End Sets.
 
 Module Type S := Sets.
@@ -335,7 +335,7 @@ Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
 
 Module Type WRawSets (E : DecidableType).
   (** First, we ask for all the functions *)
-  Include Type WOps E.
+  Include WOps E.
 
   (** Is a set well-formed or ill-formed ? *)
 
@@ -559,7 +559,7 @@ End WRaw2Sets.
 (** Same approach for ordered sets *)
 
 Module Type RawSets (E : OrderedType).
-  Include Type WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+  Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
 
   Section Spec.
   Variable s s': t.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9b5a80762..44bb02ecc 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
 Require Import NZProperties.
 
 Module ZBasePropFunct (Import Z : ZAxiomsSig').
-Include Type NZPropFunct Z.
+Include NZPropFunct Z.
 
 (* Theorems that are true for integers but not for natural numbers *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 7f2253205..9b6f0ff64 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -18,6 +18,6 @@ Require Export ZAxioms ZMulOrder.
 Module Type ZPropSig := ZMulOrderPropFunct.
 
 Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
- Include Type ZPropSig Z.
+ Include ZPropSig Z.
 End ZPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 7313c4131..97c122029 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -13,7 +13,7 @@
 Require Import NZAxioms NZBase NZMul NZOrder.
 
 Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
+Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 3c11024e5..296bd095f 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -14,7 +14,7 @@ Require Import NZAxioms NZBase NZAdd.
 
 Module Type NZMulPropSig
  (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
-Include Type NZAddPropSig NZ NZBase.
+Include NZAddPropSig NZ NZBase.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 18f61de59..7b64a6983 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -14,7 +14,7 @@ Require Import NZAxioms.
 Require Import NZAddOrder.
 
 Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZAddOrderPropSig NZ.
+Include NZAddOrderPropSig NZ.
 
 Theorem mul_lt_pred :
   forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 6697c0b3d..6a086f3bd 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -611,7 +611,6 @@ End WF.
 
 End NZOrderPropSig.
 
-Module NZOrderPropFunct (Import NZ : NZOrdSig).
- Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
-End NZOrderPropFunct.
+Module NZOrderPropFunct (NZ : NZOrdSig) :=
+ NZBasePropSig NZ <+ NZOrderPropSig NZ.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0d489a16d..842f4bcf2 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -16,7 +16,7 @@ Require Import NZProperties.
 
 Module NBasePropFunct (Import N : NAxiomsSig').
 (** First, we import all known facts about both natural numbers and integers. *)
-Include Type NZPropFunct N.
+Include NZPropFunct N.
 
 (** We prove that the successor of a number is not zero by defining a
 function (by recursion) that maps 0 to false and the successor to true *)
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 2baed54cf..30262bd9f 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -18,5 +18,5 @@ Require Export NAxioms NSub.
 Module Type NPropSig := NSubPropFunct.
 
 Module NPropFunct (N:NAxiomsSig) <: NPropSig N.
- Include Type NPropSig N.
+ Include NPropSig N.
 End NPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index ed867b825..cbbcdbff5 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -16,7 +16,7 @@ and proves its properties *)
 Require Export NSub.
 
 Module NStrongRecPropFunct (Import N : NAxiomsSig').
-Include Type NSubPropFunct N.
+Include NSubPropFunct N.
 
 Section StrongRecursion.
 
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 43df377c0..2465dc539 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -53,7 +53,7 @@ Local Infix "+" := trans_ord.
 Module Type TotalOrder_NoInline <: TotalOrder.
  Parameter Inline t : Type.
  Parameters eq lt le : t -> t -> Prop.
- Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
+ Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
 End TotalOrder_NoInline.
 
 Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
@@ -302,7 +302,7 @@ Definition t := O.t.
 Definition eq := O.eq.
 Definition lt := flip O.lt.
 Definition le := flip O.le.
-Include Type EqLtLeNotation.
+Include EqLtLeNotation.
 
 Instance eq_equiv : Equivalence eq.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index ca441fc86..1f3e50dc3 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -41,7 +41,7 @@ Module Type MiniOrderedType.
 End MiniOrderedType.
 
 Module Type OrderedType.
-  Include Type MiniOrderedType.
+  Include MiniOrderedType.
 
   (** A [eq_dec] can be deduced from [compare] below. But adding this
      redundant field allows to see an OrderedType as a DecidableType. *)
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 1cddfea3b..766b0faf0 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -43,7 +43,7 @@ Module Type LeNotation (E:EqLe).
 End LeNotation.
 
 Module Type LtLeNotation (E:EqLtLe).
-  Include Type LtNotation E <+ LeNotation E.
+  Include LtNotation E <+ LeNotation E.
   Notation "x <= y < z" := (x<=y /\ y<z).
   Notation "x < y <= z" := (x<y /\ y<=z).
 End LtLeNotation.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7955d4916..b56b0b26f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -453,6 +453,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
      else (idl,ty)) binders_ast in
   let mp = Declaremods.declare_module
     Modintern.interp_modtype Modintern.interp_modexpr
+    Modintern.interp_modexpr_or_modtype
     id binders_ast (Enforce mty_ast) []
   in
     Dumpglob.dump_moddef loc mp "mod";
@@ -493,6 +494,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
           else (idl,ty)) binders_ast in
        let mp =	Declaremods.declare_module
 	  Modintern.interp_modtype Modintern.interp_modexpr
+          Modintern.interp_modexpr_or_modtype
 	  id binders_ast mty_ast_o mexpr_ast_l
        in
 	 Dumpglob.dump_moddef loc mp "mod";
@@ -540,6 +542,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 			"and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype
+          Modintern.interp_modexpr_or_modtype
 	  id binders_ast mty_sign mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message
@@ -550,13 +553,8 @@ let vernac_end_modtype (loc,id) =
   Dumpglob.dump_modref loc mp "modtype";
   if_verbose message ("Module Type "^ string_of_id id ^" is defined")
 
-let vernac_include = function
-  | CIMTE mtys ->
-      Declaremods.declare_include
-	Modintern.interp_modtype mtys false
-  | CIME mexprs ->
-      Declaremods.declare_include
-	Modintern.interp_modexpr mexprs true
+let vernac_include l =
+  Declaremods.declare_include Modintern.interp_modexpr_or_modtype l
 
 (**********************)
 (* Gallina extensions *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2df396e09..d95fdbec9 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -176,7 +176,7 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-type module_binder = bool option * lident list * module_type_ast
+type module_binder = bool option * lident list * module_ast
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
@@ -264,12 +264,12 @@ type vernac_expr =
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
-      module_binder list * module_type_ast
+      module_binder list * module_ast
   | VernacDefineModule of bool option * lident *
-      module_binder list * module_type_ast module_signature * module_ast list
+      module_binder list * module_ast module_signature * module_ast list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_type_ast list * module_type_ast list
-  | VernacInclude of include_ast
+      module_binder list * module_ast list * module_ast list
+  | VernacInclude of module_ast list
 
   (* Solving *)