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

11 files changed, 228 insertions, 267 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index df48458e6..12ce52d1b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1012,8 +1012,8 @@ type module_type_ast =
   | CMTEwith of module_type_ast * with_declaration_ast
 
 type include_ast =
-  | CIMTE of module_type_ast
-  | CIME of module_ast
+  | CIMTE of module_type_ast * module_type_ast list
+  | CIME of module_ast * module_ast list
 
 let loc_of_notation f loc (args,_) ntn =
   if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1966bf552..1b6514a65 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -256,8 +256,8 @@ type module_type_ast =
   | CMTEwith of module_type_ast * with_declaration_ast
 
 type include_ast =
-  | CIMTE of module_type_ast
-  | CIME of module_ast
+  | CIMTE of module_type_ast * module_type_ast list
+  | CIME of module_ast * module_ast list
 
 val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
 val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c40e94c51..42d3652aa 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -663,7 +663,7 @@ let end_modtype () =
   mp
 
 
-let declare_modtype interp_modtype id args mty =
+let declare_modtype_real interp_modtype id args mty =
   let fs = Summary.freeze_summaries () in
 
   try
@@ -824,7 +824,7 @@ let rec update_include (mbids,mp,objs) =
   in
     (mbids,mp,replace_include objs)
 
-let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
+let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o =
 
   let fs = Summary.freeze_summaries () in
 
@@ -892,48 +892,42 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
     Summary.unfreeze_summaries fs; raise e
 
 
-let declare_include interp_struct me_ast is_mod is_self =
-
-  let fs = Summary.freeze_summaries () in
+let declare_one_include interp_struct me_ast is_mod is_self =
+  let env = Global.env() in
+  let me = interp_struct env me_ast in
+  let mp1,_ = current_prefix () in
+  let compute_objs objs = function
+    | MSEident mp ->
+	let mb_mp = if is_mod then
+	  Environ.lookup_module mp env else
+	    Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in
+	(match objs with
+	   |([],_,_) -> objs
+	   |(mbids,mp_self,objects) ->
+	      let mb = Global.pack_module() in
+	      let rec compute_subst mbids sign  =
+		match mbids with
+		    [] -> empty_subst
+		  | mbid::mbids ->
+		      let farg_id, farg_b, fbody_b =
+			Modops.destr_functor env sign in
+		      let subst=compute_subst mbids fbody_b in
+		      let mp_delta =
+			Modops.complete_inline_delta_resolver env mb.mod_mp
+			  farg_id farg_b mb.mod_delta in
+		      join (map_mbid mbid mb.mod_mp mp_delta) subst
+	      in
+	      let subst = compute_subst mbids mb_mp.mod_type in
+	      ([],mp_self,subst_objects subst objects))
+    | _ -> objs
+  in
 
-    try
-      let env = Global.env() in
-      let me = interp_struct env me_ast in
-      let mp1,_ = current_prefix () in
-      let compute_objs objs = function
-	| MSEident mp -> 
-	    let mb_mp = if is_mod then 
-	     Environ.lookup_module mp env else  
-	       Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in
-	      (match objs with
-		 |([],_,_) -> objs	  
-		 |(mbids,mp_self,objects) -> 
-		    let mb = Global.pack_module() in
-		    let rec compute_subst mbids sign  =
-		      match mbids with
-			  [] -> empty_subst
-			| mbid::mbids ->
-			    let farg_id, farg_b, fbody_b = 
-			      Modops.destr_functor env sign in
-			    let subst=compute_subst mbids fbody_b in
-			    let mp_delta = 
-			      Modops.complete_inline_delta_resolver env mb.mod_mp 
-				farg_id farg_b mb.mod_delta in
-			      join (map_mbid mbid mb.mod_mp mp_delta) subst
-		    in
-		    let subst = compute_subst mbids mb_mp.mod_type in
-		      ([],mp_self,subst_objects subst objects)
-		 
-	    )
-	| _ -> objs
-      in
-   
       let (mbids,mp,objs)=
 	if is_mod then
 	  get_module_substobjs env mp1 me
 	else
 	  get_modtype_substobjs env mp1 me in
-      let (mbids,mp,objs) = if is_self 
+      let (mbids,mp,objs) = if is_self
       then compute_objs (mbids,mp,objs) me else (mbids,mp,objs) in
       let id = current_mod_id() in
       let resolver =  Global.add_include me is_mod in
@@ -941,9 +935,36 @@ let declare_include interp_struct me_ast is_mod is_self =
 		       subst_objects (map_mp mp mp1 resolver) objs) in
 	ignore (add_leaf id
 		  (in_include ((me,is_mod), substobjs)))
-    with e ->
-      (* Something wrong: undo the whole process *)
-      Summary.unfreeze_summaries fs; raise e
+
+
+let declare_include interp_struct me_ast me_asts is_mod is_self =
+  let fs = Summary.freeze_summaries () in
+  try
+    declare_one_include interp_struct me_ast is_mod is_self;
+    List.iter
+      (fun me -> declare_one_include interp_struct me is_mod true)
+      me_asts
+  with e ->
+    (* Something wrong: undo the whole process *)
+    Summary.unfreeze_summaries fs; raise e
+
+
+let declare_modtype interp_mt id args = function
+  | [] -> assert false
+  | [mty] -> declare_modtype_real interp_mt id args mty
+  | mty :: mty_l ->
+      ignore (start_modtype interp_mt id args);
+      declare_include interp_mt mty mty_l false false;
+      end_modtype ()
+
+let declare_module interp_mt interp_me id args mty_o = function
+  | [] -> declare_module_real interp_mt interp_me id args mty_o None
+  | [me] -> declare_module_real interp_mt interp_me id args mty_o (Some me)
+  | me :: me_l ->
+      ignore (start_module interp_mt None id args mty_o);
+      declare_include interp_me me me_l true false;
+      end_module ()
+
 
 (*s Iterators. *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4a037b005..3d16a287f 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -40,7 +40,7 @@ val declare_module :
   (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) ->
   identifier ->
   (identifier located list * 'modtype) list -> ('modtype * bool) option ->
-  'modexpr option -> module_path
+  'modexpr list -> module_path
 
 val start_module : (env -> 'modtype -> module_struct_entry) ->
   bool option -> identifier -> (identifier located list * 'modtype) list ->
@@ -53,7 +53,8 @@ val end_module : unit -> module_path
 (*s Module types *)
 
 val declare_modtype : (env -> 'modtype -> module_struct_entry) ->
-  identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path
+  identifier -> (identifier located list * 'modtype) list ->
+  'modtype list -> module_path
 
 val start_modtype : (env -> 'modtype -> module_struct_entry) ->
   identifier -> (identifier located list * 'modtype) list -> module_path
@@ -100,7 +101,7 @@ val import_module : bool -> module_path -> unit
 (* Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry) ->
-  'struct_expr -> bool -> bool -> unit
+  'struct_expr -> 'struct_expr list -> bool -> bool -> 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 3a99b2473..38ab689f5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -389,13 +389,13 @@ GEXTEND Gram
     [ [ (* Interactive module declaration *)
         IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; mty_o = OPT of_module_type;
-	mexpr_o = OPT is_module_expr ->
-	  VernacDefineModule (export, id, bl, mty_o, mexpr_o)
-
+	o = OPT is_module_expr ->
+	  VernacDefineModule (export, id, bl, mty_o,
+			      match o with None -> [] | Some l -> l)
       | IDENT "Module"; "Type"; id = identref;
-	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
-	  VernacDeclareModuleType (id, bl, mty_o)
-
+	bl = LIST0 module_binder; o = OPT is_module_type ->
+	  VernacDeclareModuleType (id, bl,
+				   match o with None -> [] | Some l -> l)
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; ":"; mty = module_type ->
 	  VernacDeclareModule (export, id, bl, (mty,true))
@@ -413,28 +413,35 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr))
-      | IDENT "Include"; "Type"; expr = module_type ->
-          VernacInclude(false,CIMTE(expr))
-      | IDENT "Include"; "Self"; expr = module_expr ->
-          VernacInclude(true,CIME(expr))
-      | IDENT "Include"; "Self"; "Type"; expr = module_type ->
-          VernacInclude(true,CIMTE(expr)) ] ]
+      | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr ->
+	  VernacInclude(false,CIME(e,l))
+      | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type ->
+          VernacInclude(false,CIMTE(e,l))
+      | IDENT "Include"; "Self"; e = module_expr ->
+          VernacInclude(true,CIME(e,[]))
+      | IDENT "Include"; "Self"; "Type"; e = module_type ->
+          VernacInclude(true,CIMTE(e,[])) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
       | IDENT "Export" -> Some true
       |  -> None ] ]
   ;
+  ext_module_type:
+    [ [ "<+"; mty = module_type -> mty ] ]
+  ;
+  ext_module_expr:
+    [ [ "<+"; mexpr = module_expr -> mexpr ] ]
+  ;
   of_module_type:
     [ [ ":"; mty = module_type -> (mty, true)
       | "<:"; mty = module_type -> (mty, false) ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type -> mty ] ]
+    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr -> mexpr ] ]
+    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ]
   ;
 
   (* Module binder  *)
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 ": ") ++
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 7b35f4021..97ab9efc8 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2038,19 +2038,21 @@ let rec xlate_vernac =
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
-			      None ->
+			      [] ->
 				CT_coerce_ID_OPT_to_MODULE_TYPE_OPT
 				  ctv_ID_OPT_NONE
-			    | Some mty1 ->
+			    | [mty1] ->
 				CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
-				  (xlate_module_type mty1))
+				  (xlate_module_type mty1)
+	                    | _ -> failwith "TODO: Include Self")
    | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
        CT_module(xlate_ident id,
 		 xlate_module_binder_list bl,
 		 xlate_module_type_check_opt mty_o,
 		 match mexpr_o with
-		     None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
-		   | Some m -> xlate_module_expr m)
+		     [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
+		   | [m] -> xlate_module_expr m
+		   | _ -> failwith "TODO Include Self")
   | VernacDeclareModule(_,(_, id), bl, mty_o) ->
        CT_declare_module(xlate_ident id,
 		 xlate_module_binder_list bl,
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index c85e84b04..889d9c2e5 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -23,7 +23,7 @@ Local Open Scope NumScope.
     for instance [Z/nZ] (See file [NZDomain for a study of that).
 *)
 
-Module Type NZDomain_fun (Import E : EqualityType).
+Module Type NZDomain (Import E : EqualityType).
  (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *)
 
 Notation "x == y"  := (eq x y) (at level 70) : NumScope.
@@ -47,21 +47,18 @@ Axiom bi_induction :
   forall A : t -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 
-End NZDomain_fun.
+End NZDomain.
 
-Module Type NZDomainSig.
- Include Type EqualityType.
- Include Self Type NZDomain_fun.
-End NZDomainSig.
+Module Type NZDomainSig := EqualityType <+ NZDomain.
+
+(** A version with decidable type *)
+
+Module Type NZDecDomainSig := DecidableType <+ NZDomain.
 
-Module Type NZDecDomainSig.
- Include Type DecidableType.
- Include Self Type NZDomain_fun.
-End NZDecDomainSig.
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
-Module Type NZBasicFuns_fun (Import NZ : NZDomainSig).
+Module Type NZHasBasicFuns (Import NZ : NZDomainSig).
 
 Parameter Inline add : t -> t -> t.
 Parameter Inline sub : t -> t -> t.
@@ -84,12 +81,10 @@ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
 Axiom mul_0_l : forall n, 0 * n == 0.
 Axiom mul_succ_l : forall n m, S n * m == n * m + m.
 
-End NZBasicFuns_fun.
+End NZHasBasicFuns.
+
+Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns.
 
-Module Type NZBasicFunsSig.
- Include Type NZDomainSig.
- Include Self Type NZBasicFuns_fun.
-End NZBasicFunsSig.
 
 (** Old name for the same interface: *)
 
@@ -98,7 +93,7 @@ Module Type NZAxiomsSig := NZBasicFunsSig.
 
 (** Axiomatization of order *)
 
-Module Type NZOrd_fun (Import NZ : NZDomainSig).
+Module Type NZHasOrd (Import NZ : NZDomainSig).
 
 Parameter Inline lt : t -> t -> Prop.
 Parameter Inline le : t -> t -> Prop.
@@ -116,17 +111,14 @@ Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irrefl : forall n, ~ (n < n).
 Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
 
-End NZOrd_fun.
+End NZHasOrd.
 
-Module Type NZOrdSig.
- Include Type NZDomainSig.
- Include Self Type NZOrd_fun.
-End NZOrdSig.
+Module Type NZOrdSig := NZDomainSig <+ NZHasOrd.
 
 
 (** Axiomatization of minimum and maximum *)
 
-Module Type NZMinMax_fun (Import NZ : NZOrdSig).
+Module Type NZHasMinMax (Import NZ : NZOrdSig).
 
 Parameter Inline min : t -> t -> t.
 Parameter Inline max : t -> t -> t.
@@ -138,11 +130,9 @@ Axiom min_r : forall n m, m <= n -> min n m == m.
 Axiom max_l : forall n m, m <= n -> max n m == n.
 Axiom max_r : forall n m, n <= m -> max n m == m.
 
-End NZMinMax_fun.
+End NZHasMinMax.
+
+
+Module Type NZOrdAxiomsSig :=
+ NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax.
 
-Module Type NZOrdAxiomsSig.
- Include Type NZDomainSig.
- Include Self Type NZBasicFuns_fun.
- Include Self Type NZOrd_fun.
- Include Self Type NZMinMax_fun.
-End NZOrdAxiomsSig.
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 7cae4358b..111f45ca7 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -22,135 +22,98 @@ End BareEquality.
 
 (** * Specification of the equality by the Type Classe [Equivalence] *)
 
-Module Type Equality_fun (Import E:BareEquality).
+Module Type IsEq (Import E:BareEquality).
   Instance eq_equiv : Equivalence eq.
   Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
-End Equality_fun.
+End IsEq.
 
 (** * Earlier specification of equality by three separate lemmas. *)
 
-Module Type EqualityOrig_fun(Import E:BareEquality).
+Module Type IsEqOrig (Import E:BareEquality).
   Axiom eq_refl : forall x : t, eq x x.
   Axiom eq_sym : forall x y : t, eq x y -> eq y x.
   Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
-End EqualityOrig_fun.
+End IsEqOrig.
 
 (** * Types with decidable equality *)
 
-Module Type Decidable_fun (Import E:BareEquality).
+Module Type HasEqDec (Import E:BareEquality).
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
-End Decidable_fun.
+End HasEqDec.
 
 (** * Boolean Equality *)
 
 (** Having [eq_dec] is the same as having a boolean equality plus
     a correctness proof. *)
 
-Module Type BoolEq_fun (Import E:BareEquality).
+Module Type HasEqBool (Import E:BareEquality).
   Parameter Inline eqb : t -> t -> bool.
   Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
-End BoolEq_fun.
+End HasEqBool.
 
 (** From these basic blocks, we can build many combinations
     of static standalone module types. *)
 
-Module Type EqualityType.
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-End EqualityType.
-
-Module Type EqualityTypeOrig.
-  Include Type BareEquality.
-  Include Self Type EqualityOrig_fun.
-End EqualityTypeOrig.
-
-Module Type EqualityTypeBoth. (* <: EqualityType <: EqualityTypeOrig *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type EqualityOrig_fun.
-End EqualityTypeBoth.
-
-Module Type DecidableType. (* <: EqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type Decidable_fun.
-End DecidableType.
-
-Module Type DecidableTypeOrig. (* <: EqualityTypeOrig *)
-  Include Type BareEquality.
-  Include Self Type EqualityOrig_fun.
-  Include Self Type Decidable_fun.
-End DecidableTypeOrig.
-
-Module Type DecidableTypeBoth. (* <: DecidableType <: DecidableTypeOrig *)
-  Include Type EqualityTypeBoth.
-  Include Self Type Decidable_fun.
-End DecidableTypeBoth.
-
-Module Type BooleanEqualityType. (* <: EqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type BoolEq_fun.
-End BooleanEqualityType.
-
-Module Type BooleanDecidableType. (* <: DecidableType <: BooleanEqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type Decidable_fun.
-  Include Self Type BoolEq_fun.
-End BooleanDecidableType.
-
-Module Type DecidableTypeFull. (* <: all previous interfaces *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type EqualityOrig_fun.
-  Include Self Type Decidable_fun.
-  Include Self Type BoolEq_fun.
-End DecidableTypeFull.
+Module Type EqualityType := BareEquality <+ IsEq.
+
+Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig.
+
+Module Type EqualityTypeBoth (* <: EqualityType <: EqualityTypeOrig *)
+ := BareEquality <+ IsEq <+ IsEqOrig.
+
+Module Type DecidableType (* <: EqualityType *)
+ := BareEquality <+ IsEq <+ HasEqDec.
+
+Module Type DecidableTypeOrig (* <: EqualityTypeOrig *)
+ := BareEquality <+ IsEqOrig <+ HasEqDec.
+
+Module Type DecidableTypeBoth (* <: DecidableType <: DecidableTypeOrig *)
+ := EqualityTypeBoth <+ HasEqDec.
+
+Module Type BooleanEqualityType (* <: EqualityType *)
+ := BareEquality <+ IsEq <+ HasEqBool.
+
+Module Type BooleanDecidableType (* <: DecidableType <: BooleanEqualityType *)
+ := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool.
+
+Module Type DecidableTypeFull (* <: all previous interfaces *)
+ := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
 (** * Compatibility wrapper from/to the old version of
       [EqualityType] and [DecidableType] *)
 
-Module Backport_ET_fun (E:BareEquality)(F:Equality_fun E) <: EqualityOrig_fun E.
+Module BackportEq (E:BareEquality)(F:IsEq E) <: IsEqOrig E.
  Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
  Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
  Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
-End Backport_ET_fun.
+End BackportEq.
 
-Module Update_ET_fun (E:BareEquality)(F:EqualityOrig_fun E) <: Equality_fun E.
+Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
  Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
-End Update_ET_fun.
+End UpdateEq.
 
-Module Backport_ET (E:EqualityType) <: EqualityTypeBoth.
- Include E.
- Include Backport_ET_fun E E.
-End Backport_ET.
+Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
+ := E <+ BackportEq E E.
 
-Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth.
- Include E.
- Include Update_ET_fun E E.
-End Update_ET.
+Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
+ := E <+ UpdateEq E E.
 
-Module Backport_DT (E:DecidableType) <: DecidableTypeBoth.
- Include E.
- Include Backport_ET_fun E E.
-End Backport_DT.
+Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
+ := E <+ BackportEq E E.
 
-Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth.
- Include E.
- Include Update_ET_fun E E.
-End Update_DT.
+Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
+ := E <+ UpdateEq E E.
 
 
 (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
 
-Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E.
+Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E.
  Definition eqb x y := if F.eq_dec x y then true else false.
  Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
  Proof.
@@ -158,9 +121,9 @@ Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E.
   auto with *.
   split. discriminate. intro EQ; elim NEQ; auto.
  Qed.
-End Dec2Bool_fun.
+End HasEqDec2Bool.
 
-Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E.
+Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E.
  Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
  Proof.
   intros x y. assert (H:=F.eqb_eq x y).
@@ -168,17 +131,13 @@ Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E.
   apply -> H; auto.
   intro EQ. apply H in EQ. discriminate.
  Defined.
-End Bool2Dec_fun.
+End HasEqBool2Dec.
 
-Module Dec2Bool (E:DecidableType) <: BooleanDecidableType.
- Include E.
- Include Dec2Bool_fun E E.
-End Dec2Bool.
+Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
+ := E <+ HasEqDec2Bool E E.
 
-Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType.
- Include E.
- Include Bool2Dec_fun E E.
-End Bool2Dec.
+Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
+ := E <+ HasEqBool2Dec E E.
 
 
 
@@ -192,46 +151,30 @@ Module Type UsualBareEquality. (* <: BareEquality *)
  Definition eq := @eq t.
 End UsualBareEquality.
 
-Module UsualEquality_fun (E:UsualBareEquality) <: Equality_fun E.
+Module UsualIsEq (E:UsualBareEquality) <: IsEq E.
  Program Instance eq_equiv : Equivalence E.eq.
-End UsualEquality_fun.
+End UsualIsEq.
 
-Module UsualEqualityOrig_fun (E:UsualBareEquality) <: EqualityOrig_fun E.
+Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E.
  Definition eq_refl := @eq_refl E.t.
  Definition eq_sym := @eq_sym E.t.
  Definition eq_trans := @eq_trans E.t.
-End UsualEqualityOrig_fun.
-
-Module Type UsualEqualityType. (* <: EqualityType *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
-End UsualEqualityType.
-
-Module Type UsualDecidableType. (* <: DecidableType *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type Decidable_fun.
-End UsualDecidableType.
-
-Module Type UsualDecidableTypeBoth. (* <: DecidableTypeBoth *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type EqualityOrig_fun.
- Include Self Type Decidable_fun.
-End UsualDecidableTypeBoth.
-
-Module Type UsualBoolEq.
- Include Type UsualBareEquality.
- Include Self Type BoolEq_fun.
-End UsualBoolEq.
-
-Module Type UsualDecidableTypeFull. (* <: DecidableTypeFull *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type EqualityOrig_fun.
- Include Self Type Decidable_fun.
- Include Self Type BoolEq_fun.
-End UsualDecidableTypeFull.
+End UsualIsEqOrig.
+
+Module Type UsualEqualityType (* <: EqualityType *)
+ := UsualBareEquality <+ IsEq.
+
+Module Type UsualDecidableType (* <: DecidableType *)
+ := UsualBareEquality <+ IsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeBoth (* <: DecidableTypeBoth *)
+ := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec.
+
+Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool.
+
+Module Type UsualDecidableTypeFull (* <: DecidableTypeFull *)
+ := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+
 
 (** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
@@ -247,14 +190,10 @@ End MiniDecidableType.
 Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
  Include M.
  Definition eq := @eq M.t.
- Include Self UsualEquality_fun.
- Include Self UsualEqualityOrig_fun.
+ Include Self UsualIsEq.
+ Include Self UsualIsEqOrig.
 End Make_UDT.
 
-Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull.
- Include M. (* t, eq, eqb, eqb_eq *)
- Include UsualEquality_fun M.
- Include UsualEqualityOrig_fun M.
- Include Bool2Dec_fun M M.
-End Make_UDTF.
+Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
+ := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2008e5f01..76e7eb0b8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -460,19 +460,19 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
      else (idl,ty)) binders_ast in
   let mp = Declaremods.declare_module
     Modintern.interp_modtype Modintern.interp_modexpr
-    id binders_ast (Some mty_ast_o) None
+    id binders_ast (Some mty_ast_o) []
   in
     Dumpglob.dump_moddef loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is declared");
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
-let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
+let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections.";
-  match mexpr_ast_o with
-    | None ->
+  match mexpr_ast_l with
+    | [] ->
        check_no_pending_proofs ();
        let binders_ast,argsexport =
         List.fold_right
@@ -490,7 +490,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
              Option.iter
                (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
            ) argsexport
-    | Some _ ->
+    | _::_ ->
        let binders_ast = List.map
         (fun (export,idl,ty) ->
           if export <> None then
@@ -500,7 +500,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
           else (idl,ty)) binders_ast in
        let mp =	Declaremods.declare_module
 	  Modintern.interp_modtype Modintern.interp_modexpr
-	  id binders_ast mty_ast_o mexpr_ast_o
+	  id binders_ast mty_ast_o mexpr_ast_l
        in
 	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message
@@ -514,12 +514,12 @@ let vernac_end_module export (loc,id as lid) =
   if_verbose message ("Module "^ string_of_id id ^" is defined") ;
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
-let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
+let vernac_declare_module_type (loc,id) binders_ast mty_ast_l =
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections.";
 
-  match mty_ast_o with
-    | None ->
+  match mty_ast_l with
+    | [] ->
        check_no_pending_proofs ();
        let binders_ast,argsexport =
         List.fold_right
@@ -536,7 +536,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
             (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
          ) argsexport
 
-    | Some base_mty ->
+    | _ :: _ ->
 	let binders_ast = List.map
           (fun (export,idl,ty) ->
             if export <> None then
@@ -545,7 +545,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
 			"and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype
-	  id binders_ast base_mty in
+	  id binders_ast mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message
 	    ("Module Type "^ string_of_id id ^" is defined")
@@ -556,12 +556,12 @@ let vernac_end_modtype (loc,id) =
   if_verbose message ("Module Type "^ string_of_id id ^" is defined")
 
 let vernac_include is_self = function
-  | CIMTE mty_ast ->
+  | CIMTE (mty,mtys) ->
       Declaremods.declare_include
-	Modintern.interp_modtype mty_ast false is_self
-  | CIME mexpr_ast ->
+	Modintern.interp_modtype mty mtys false is_self
+  | CIME (mexpr, mexprs) ->
       Declaremods.declare_include
-	Modintern.interp_modexpr mexpr_ast true is_self
+	Modintern.interp_modexpr mexpr mexprs true is_self
 
 (**********************)
 (* Gallina extensions *)
@@ -1329,12 +1329,12 @@ let interp c = match c with
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
       vernac_declare_module export lid bl mtyo
-  | VernacDefineModule (export,lid,bl,mtyo,mexpro) ->
-      vernac_define_module export lid bl mtyo mexpro
+  | VernacDefineModule (export,lid,bl,mtyo,mexprl) ->
+      vernac_define_module export lid bl mtyo mexprl
   | VernacDeclareModuleType (lid,bl,mtyo) ->
       vernac_declare_module_type lid bl mtyo
-  | VernacInclude (is_self,in_ast) ->
-      vernac_include is_self in_ast
+  | VernacInclude (is_self,in_asts) ->
+      vernac_include is_self in_asts
   (* Gallina extensions *)
   | VernacBeginSection lid -> vernac_begin_section lid
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 366308bfa..ccb850651 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -261,9 +261,9 @@ type vernac_expr =
   | VernacDeclareModule of bool option * lident *
       module_binder list * (module_type_ast * bool)
   | VernacDefineModule of bool option * lident *
-      module_binder list * (module_type_ast * bool) option * module_ast option
+      module_binder list * (module_type_ast * bool) option * module_ast list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_type_ast option
+      module_binder list * module_type_ast list
   | VernacInclude of bool * include_ast
 
   (* Solving *)