Module subtyping : allow many <: and module type declaration with <:

 Any place where <: was legal can now contain many <: declarations.
 Moreover we can say that the module type we are declaring is a subtype
 of an earlier module type. See DecidableType2 for examples.
 Also try to handle correctly the freeze/unfreeze summaries
 when simulating start/include/end (syntax ... := ... <+ ...)

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

12 files changed, 252 insertions, 231 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 12ce52d1b..a6b4b1b0a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1001,7 +1001,6 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-
 type module_ast =
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
@@ -1015,6 +1014,10 @@ type include_ast =
   | CIMTE of module_type_ast * module_type_ast list
   | CIME of module_ast * module_ast list
 
+type 'a module_signature =
+  | Enforce of 'a (* ... : T *)
+  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+
 let loc_of_notation f loc (args,_) ntn =
   if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
   else snd (Util.unloc (f (List.hd args)))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1b6514a65..1c0b207ea 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -245,7 +245,6 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-
 type module_ast =
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
@@ -259,5 +258,9 @@ type include_ast =
   | CIMTE of module_type_ast * module_type_ast list
   | CIME of module_ast * module_ast list
 
+type 'a module_signature =
+  | Enforce of 'a (* ... : T *)
+  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+
 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 42d3652aa..0ed617a0b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -77,10 +77,10 @@ let modtab_objects =
 
 (* currently started interactive module (if any) - its arguments (if it
    is a functor) and declared output type *)
-let openmod_info = 
-  ref ((MPfile(initial_dir),[],None,None) 
-	 : module_path *  mod_bound_id list * module_struct_entry option 
-                                          * module_type_body option) 
+let openmod_info =
+  ref ((MPfile(initial_dir),[],None,[])
+	 : module_path *  mod_bound_id list * module_struct_entry option
+                                          * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -101,7 +101,7 @@ let _ = Summary.declare_summary "MODULE-INFO"
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
 				       openmod_info := ((MPfile(initial_dir),
-							 [],None,None));
+							 [],None,[]));
 				       library_cache := Dirmap.empty) }
 
 (* auxiliary functions to transform full_path and kernel_name given
@@ -118,17 +118,58 @@ let dir_of_sp sp =
   let dir,id = repr_path sp in
     add_dirpath_suffix dir id
 
+(* Subtyping checks *)
+
+let check_sub mtb sub_mtb_l =
+  (* The constraints are checked and forgot immediately : *)
+  ignore (List.fold_right
+	    (fun sub_mtb env ->
+	       Environ.add_constraints
+		 (Subtyping.check_subtypes env mtb sub_mtb) env)
+	    sub_mtb_l (Global.env()))
 
 (* This function checks if the type calculated for the module [mp] is
-   a subtype of [sub_mtb]. Uses only the global environment. *)
-let check_subtypes mp sub_mtb =
+   a subtype of all signatures in [sub_mtb_l]. Uses only the global
+   environment. *)
+
+let check_subtypes mp sub_mtb_l =
   let env = Global.env () in
   let mb = Environ.lookup_module mp env in
   let mtb = Modops.module_type_of_module env None mb in
-  let _ = Environ.add_constraints 
-    (Subtyping.check_subtypes env mtb sub_mtb) 
-  in
-    ()  (* The constraints are checked and forgot immediately! *)
+  check_sub mtb sub_mtb_l
+
+(* Same for module type [mp] *)
+
+let check_subtypes_mt mp sub_mtb_l =
+  check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l
+
+(* Create a functor type entry *)
+
+let funct_entry args m =
+  List.fold_right
+    (fun (arg_id,arg_t) mte -> MSEfunctor (arg_id,arg_t,mte))
+    args m
+
+(* Prepare the module type list for check of subtypes *)
+
+let build_subtypes interp_modtype mp args mtys =
+  List.map
+    (fun m ->
+       let mte = interp_modtype (Global.env()) m in
+       let mtb = Mod_typing.translate_module_type (Global.env()) mp mte in
+       let funct_mtb =
+	 List.fold_right
+           (fun (arg_id,arg_t) mte ->
+              let arg_t =
+		Mod_typing.translate_module_type (Global.env())
+		  (MPbound arg_id) arg_t
+	      in
+              SEBfunctor(arg_id,arg_t,mte))
+           args mtb.typ_expr
+       in
+       { mtb with typ_expr = funct_mtb })
+    mtys
+
 
 (* These functions register the visibility of the module and iterates
    through its components. They are called by plenty module functions *)
@@ -266,7 +307,7 @@ let modtypetab =
 (* currently started interactive module type. We remember its arguments
    if it is a functor type *)
 let openmodtype_info =
-  ref ([] : mod_bound_id list)
+  ref ([],[] : mod_bound_id list * module_type_body list)
 
 let _ = Summary.declare_summary "MODTYPE-INFO"
 	  { Summary.freeze_function = (fun () ->
@@ -276,30 +317,35 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
 					   openmodtype_info := snd ft);
 	    Summary.init_function = (fun () ->
 				       modtypetab := MPmap.empty;
-				       openmodtype_info := []) }
+				       openmodtype_info := [],[]) }
+
 
+let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
+  let mp = mp_of_kn kn in
 
-let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
   let _ =
     match entry with
       | None ->
 	  anomaly "You must not recache interactive module types!"
       | Some mte ->
-	  let mp = Global.add_modtype (basename sp) mte in
-	  if mp <>mp_of_kn kn then
+	  if mp <> Global.add_modtype (basename sp) mte then
 	    anomaly "Kernel and Library names do not match"
   in
 
+  (* Using declare_modtype should lead here, where we check
+     that any given subtyping is indeed accurate *)
+  check_subtypes_mt mp sub_mty_l;
+
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
       (pr_path sp ++ str " already exists") ;
 
-  Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn);
+  Nametab.push_modtype (Nametab.Until 1) sp mp;
 
-  modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
+  modtypetab := MPmap.add mp modtypeobjs !modtypetab
 
 
-let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
+let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
   check_empty "load_modtype" entry;
 
   if Nametab.exists_modtype sp then
@@ -311,7 +357,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
   modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
 
 
-let open_modtype i ((sp,kn),(entry,_)) =
+let open_modtype i ((sp,kn),(entry,_,_)) =
   check_empty "open_modtype" entry;
 
   if
@@ -323,13 +369,13 @@ let open_modtype i ((sp,kn),(entry,_)) =
 
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
-let subst_modtype (subst,(entry,(mbids,mp,objs))) =
+let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
   check_empty "subst_modtype" entry;
-  (entry,(mbids,subst_mp subst mp,subst_objects subst objs))
+  (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
 
-let classify_modtype (_,substobjs) =
-  Substitute (None,substobjs)
+let classify_modtype (_,substobjs,_) =
+  Substitute (None,substobjs,[])
 
 
 let (in_modtype,_) =
@@ -448,36 +494,19 @@ let intern_args interp_modtype (idl,arg) =
 	 (mbid,mty))
     dirs mbids
 
-let start_module interp_modtype export id args res_o =
-  let fs = Summary.freeze_summaries () in
+let start_module_ interp_modtype export id args res fs =
   let mp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-  let res_entry_o, sub_body_o = match res_o with
-      None -> None, None
-    | Some (res, restricted) ->
-	(* we translate the module here to catch errors as early as possible *)
+  let res_entry_o, sub_body_l = match res with
+    | Topconstr.Enforce res ->
 	let mte = interp_modtype (Global.env()) res in
-	  if restricted then
-	    let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in
-	      Some mte, None
-	  else
-	    let mtb = Mod_typing.translate_module_type (Global.env())
-	      mp mte in
-	    let funct_mtb = 
-	      List.fold_right 
-		(fun (arg_id,arg_t) mte -> 
-		let arg_t = Mod_typing.translate_module_type (Global.env())
-		  (MPbound arg_id)  arg_t
-		in
-		  SEBfunctor(arg_id,arg_t,mte))
-		arg_entries mtb.typ_expr
-	    in
-	      None, Some {mtb with 
-			 typ_expr = funct_mtb}
+	let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in
+	Some mte, []
+    | Topconstr.Check resl ->
+	None, build_subtypes interp_modtype mp arg_entries resl
   in
-
   let mbids = List.map fst arg_entries in
-    openmod_info:=(mp,mbids,res_entry_o,sub_body_o);
+  openmod_info:=(mp,mbids,res_entry_o,sub_body_l);
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
   Lib.add_frozen_state (); mp
@@ -486,7 +515,7 @@ let start_module interp_modtype export id args res_o =
 let end_module () =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
-  let mp,mbids, res_o, sub_o = !openmod_info in
+  let mp,mbids, res_o, sub_l = !openmod_info in
   let substitute, keep, special = Lib.classify_segment lib_stack in
 
   let mp_from,substobjs, keep, special = try
@@ -514,10 +543,7 @@ let end_module () =
   let id = basename (fst oldoname) in
   let mp,resolver = Global.end_module fs id res_o in
 
-  begin match sub_o with
-      None -> ()
-    | Some sub_mtb -> check_subtypes mp sub_mtb
-  end;
+  check_subtypes mp sub_l;
 
 (* we substitute objects if the module is 
    sealed by a signature (ie. mp_from != None *)
@@ -581,7 +607,7 @@ let register_library dir cenv objs digest =
 
 let start_library dir =
   let mp = Global.start_library dir in
-  openmod_info:=mp,[],None,None;
+  openmod_info:=mp,[],None,[];
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
@@ -630,14 +656,13 @@ let import_module export mp =
 
 (************************************************************************)
 (* module types *)
-let start_modtype interp_modtype id args =
-  let fs = Summary.freeze_summaries () in
 
+let start_modtype_ interp_modtype id args mtys fs =
   let mp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
+  let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in
   let mbids = List.map fst arg_entries in
-  openmodtype_info := mbids;
+  openmodtype_info := mbids, sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
   Lib.add_frozen_state (); mp
@@ -647,11 +672,12 @@ let end_modtype () =
   let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
   let id = basename (fst oldoname) in
   let substitute, _, special = Lib.classify_segment lib_stack in
-  let mbids = !openmodtype_info in
+  let mbids, sub_mty_l = !openmodtype_info in
   let mp = Global.end_modtype fs id in
-  let modtypeobjs = mbids, mp, substitute in  
-  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
-
+  let modtypeobjs = mbids, mp, substitute in
+  check_subtypes_mt mp sub_mty_l;
+  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])])
+  in
   if fst oname <> fst oldoname then
     anomaly
       "Section paths generated on start_ and end_modtype do not match";
@@ -663,32 +689,23 @@ let end_modtype () =
   mp
 
 
-let declare_modtype_real interp_modtype id args mty =
-  let fs = Summary.freeze_summaries () in
-
-  try
+let declare_modtype_ interp_modtype id args mtys mty fs =
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let base_mty = interp_modtype (Global.env()) mty in
-  let entry =
-    List.fold_right
-      (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-      arg_entries
-      base_mty
-  in
+  let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
+  (* NB: check of subtyping will be done in cache_modtype *)
+  let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in
   let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp entry in
-    (* Undo the simulated interactive building of the module type *)
-    (* and declare the module type as a whole *)
+  (* Undo the simulated interactive building of the module type *)
+  (* and declare the module type as a whole *)
 
   let substobjs = (mbids,mmp,
-		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in
-    Summary.unfreeze_summaries fs;
-    ignore (add_leaf id (in_modtype (Some entry, substobjs)));
-    mmp
-  with e ->
-    (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
+		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs)
+  in
+  Summary.unfreeze_summaries fs;
+  ignore (add_leaf id (in_modtype (Some entry, substobjs, sub_mty_l)));
+  mmp
+
 
 (* Small function to avoid module typing during substobjs retrivial  *)
 let rec get_objs_module_application env = function
@@ -824,36 +841,16 @@ let rec update_include (mbids,mp,objs) =
   in
     (mbids,mp,replace_include objs)
 
-let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o =
-
-  let fs = Summary.freeze_summaries () in
-
-  try
+let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   let mmp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
-  let mty_entry_o, mty_sub_o = match mty_o with
-      None -> None, None
-    | (Some (mty, true)) ->
-	Some (List.fold_right
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries
-		(interp_modtype (Global.env()) mty)),
-	None
-    | (Some (mty, false)) ->
-	None,
-	Some (List.fold_right
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries
-		(interp_modtype (Global.env()) mty))
+  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
+  let mty_entry_o, mty_sub_l = match res with
+    | Topconstr.Enforce mty -> Some (funct interp_modtype mty), []
+    | Topconstr.Check mtys -> None, List.map (funct interp_modtype) mtys
   in
-  let mexpr_entry_o = match mexpr_o with
-      None -> None
-    | Some mexpr ->
-	Some (List.fold_right
-		(fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
-		arg_entries
-		(interp_modexpr (Global.env()) mexpr))  in
+  let mexpr_entry_o = Option.map (funct interp_modexpr) mexpr_o in
   let entry =
     {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
@@ -866,30 +863,23 @@ let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o =
       | _ -> anomaly "declare_module: No type, no body ..."
   in
   let (mbids,mp_from,objs) = update_include substobjs in
-    (* Undo the simulated interactive building of the module *)
-    (* and declare the module as a whole *)
-    Summary.unfreeze_summaries fs;
-    let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-    let mp_env,resolver = Global.add_module id entry in
-    let _ = if mp_env <> mp then
-      anomaly "Kernel and Library names do not match";
-      match  mty_sub_o with
-	| None -> ()
-	| Some sub_mte -> 
-	    let sub_mtb = Mod_typing.translate_module_type
-	      env mp sub_mte in
-	      check_subtypes mp_env sub_mtb
-    in
-    let substobjs = (mbids,mp_env,
-		     subst_objects(map_mp mp_from mp_env resolver) objs) in
-      ignore (add_leaf
-		id
-		(in_module (Some (entry, mty_sub_o), substobjs)));
-      mmp
-	
-  with e -> 
-    (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
+  (* Undo the simulated interactive building of the module *)
+  (* and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+  let mp_env,resolver = Global.add_module id entry in
+
+  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+
+  let subs = List.map (Mod_typing.translate_module_type env mp) mty_sub_l in
+  check_subtypes mp subs;
+
+  let substobjs = (mbids,mp_env,
+		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  ignore (add_leaf
+	    id
+	    (in_module (Some (entry), substobjs)));
+  mmp
 
 
 let declare_one_include interp_struct me_ast is_mod is_self =
@@ -937,33 +927,53 @@ let declare_one_include interp_struct me_ast is_mod is_self =
 		  (in_include ((me,is_mod), substobjs)))
 
 
-let declare_include interp_struct me_ast me_asts is_mod is_self =
+let declare_include_ interp_struct me_ast me_asts is_mod is_self =
+  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
+
+(** Versions of earlier functions taking care of the freeze/unfreeze
+    of summaries *)
+
+let protect_summaries f =
   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
+  try f fs
   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 =
+  protect_summaries
+    (fun _ -> declare_include_ interp_struct me_ast me_asts is_mod is_self)
+
+let declare_modtype interp_mt 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 :: mty_l ->
+	ignore (start_modtype_ interp_mt id args mtys fs);
+	declare_include_ interp_mt mty mty_l false false;
+	end_modtype ()
+  in
+  protect_summaries declare_mt
+
+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_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 :: me_l ->
+	ignore (start_module_ interp_mt None id args mtys fs);
+	declare_include_ interp_me me me_l true false;
+	end_module ()
+  in
+  protect_summaries declare_me
 
-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 ()
+let start_module interp_modtype export id args res =
+ protect_summaries (start_module_ interp_modtype export id args res)
 
 
 (*s Iterators. *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 3d16a287f..f20be9cd0 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -37,14 +37,16 @@ open Lib
 *)
 
 val declare_module :
-  (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) ->
+  (env -> 'modtype -> module_struct_entry) ->
+  (env -> 'modexpr -> module_struct_entry) ->
   identifier ->
-  (identifier located list * 'modtype) list -> ('modtype * bool) option ->
+  (identifier located list * 'modtype) list ->
+  'modtype Topconstr.module_signature ->
   'modexpr list -> module_path
 
 val start_module : (env -> 'modtype -> module_struct_entry) ->
   bool option -> identifier -> (identifier located list * 'modtype) list ->
-   ('modtype * bool) option -> module_path
+  'modtype Topconstr.module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -54,10 +56,11 @@ val end_module : unit -> module_path
 
 val declare_modtype : (env -> 'modtype -> module_struct_entry) ->
   identifier -> (identifier located list * 'modtype) list ->
-  'modtype list -> module_path
+  'modtype list -> 'modtype list -> module_path
 
 val start_modtype : (env -> 'modtype -> module_struct_entry) ->
-  identifier -> (identifier located list * 'modtype) list -> module_path
+  identifier -> (identifier located list * 'modtype) list ->
+  'modtype list -> module_path
 
 val end_modtype : unit -> module_path
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 38ab689f5..56946ef27 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -388,17 +388,16 @@ GEXTEND Gram
   gallina_ext:
     [ [ (* Interactive module declaration *)
         IDENT "Module"; export = export_token; id = identref;
-	bl = LIST0 module_binder; mty_o = OPT of_module_type;
-	o = OPT is_module_expr ->
-	  VernacDefineModule (export, id, bl, mty_o,
-			      match o with None -> [] | Some l -> l)
+	bl = LIST0 module_binder; sign = of_module_type;
+	body = is_module_expr ->
+	  VernacDefineModule (export, id, bl, sign, body)
       | IDENT "Module"; "Type"; id = identref;
-	bl = LIST0 module_binder; o = OPT is_module_type ->
-	  VernacDeclareModuleType (id, bl,
-				   match o with None -> [] | Some l -> l)
+	bl = LIST0 module_binder; sign = check_module_types;
+	body = is_module_type ->
+	  VernacDeclareModuleType (id, bl, sign, body)
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
 	bl = LIST0 module_binder; ":"; mty = module_type ->
-	  VernacDeclareModule (export, id, bl, (mty,true))
+	  VernacDeclareModule (export, id, bl, mty)
       (* Section beginning *)
       | IDENT "Section"; id = identref -> VernacBeginSection id
       | IDENT "Chapter"; id = identref -> VernacBeginSection id
@@ -433,15 +432,23 @@ GEXTEND Gram
   ext_module_expr:
     [ [ "<+"; mexpr = module_expr -> mexpr ] ]
   ;
+  check_module_type:
+    [ [ "<:"; mty = module_type -> mty ] ]
+  ;
+  check_module_types:
+    [ [ mtys = LIST0 check_module_type -> mtys ] ]
+  ;
   of_module_type:
-    [ [ ":"; mty = module_type -> (mty, true)
-      | "<:"; mty = module_type -> (mty, false) ] ]
+    [ [ ":"; mty = module_type -> Enforce mty
+      | mtys = check_module_types -> Check mtys ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ]
+    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l)
+      | -> [] ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ]
+    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l)
+      | -> [] ] ]
   ;
 
   (* Module binder  *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4407ca6aa..190271159 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -253,9 +253,10 @@ and  pr_module_expr = function
       pr_module_expr me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
-let pr_of_module_type prc (mty,b) =
-  str (if b then ":" else "<:") ++
-  pr_module_type prc mty
+let pr_of_module_type prc = function
+  | Enforce mty -> str ":" ++ pr_module_type prc mty
+  | Check mtys ->
+      prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys
 
 let pr_require_token = function
   | Some true -> str "Export "
@@ -746,24 +747,25 @@ let rec pr_vernac = function
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id)
 
   (* Modules and Module Types *)
-  | VernacDefineModule (export,m,bl,ty,bd) ->
+  | VernacDefineModule (export,m,bl,tys,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in
       hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
                pr_lident m ++ b ++
-               pr_opt (pr_of_module_type pr_lconstr) ty ++
+               pr_of_module_type pr_lconstr tys ++
 	       (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 ++
              pr_lident id ++ b ++
-             pr_of_module_type pr_lconstr m1)
-  | VernacDeclareModuleType (id,bl,m) ->
+             pr_module_type 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
 	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_module_type pr_lconstr) m)
+		 prlist_with_sep (fun () -> str " <+ ") pr_mt 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 " ++
diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli
index bc615f14e..bd82688d3 100644
--- a/plugins/interface/ascent.mli
+++ b/plugins/interface/ascent.mli
@@ -479,7 +479,7 @@ and ct_MODULE_TYPE =
   | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
 and ct_MODULE_TYPE_CHECK =
     CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
-  | CT_only_check of ct_MODULE_TYPE
+  | CT_only_check of ct_MODULE_TYPE list
 and ct_MODULE_TYPE_OPT =
     CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT
   | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE
diff --git a/plugins/interface/vtp.ml b/plugins/interface/vtp.ml
index a84f9ea56..d71336150 100644
--- a/plugins/interface/vtp.ml
+++ b/plugins/interface/vtp.ml
@@ -1185,9 +1185,9 @@ and fMODULE_TYPE = function
    fNODE "module_type_with_mod" 3
 and fMODULE_TYPE_CHECK = function
 | CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x
-| CT_only_check(x1) ->
-   fMODULE_TYPE x1 ++
-   fNODE "only_check" 1
+| CT_only_check(l) ->
+   (List.fold_left (++) (mt()) (List.map fMODULE_TYPE l)) ++
+   fNODE "only_check" (List.length l)
 and fMODULE_TYPE_OPT = function
 | CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x
 | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 97ab9efc8..9ba1d6715 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1617,14 +1617,13 @@ let xlate_module_binder_list (l:module_binder list) =
 		 CT_module_binder
 		   (CT_id_ne_list(fst, idl2), xlate_module_type mty)) l);;
 
-let xlate_module_type_check_opt = function
-    None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
- 	(CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE)
-  | Some(mty, true) -> CT_only_check(xlate_module_type mty)
-  | Some(mty, false) ->
+let xlate_module_type_check = function
+  | Topconstr.Enforce mty ->
       CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
 	(CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
-	   (xlate_module_type mty));;
+	   (xlate_module_type mty))
+  | Topconstr.Check mtys ->
+      CT_only_check (List.map xlate_module_type mtys)
 
 let rec xlate_module_expr = function
     CMEident (_, qid) -> CT_coerce_ID_OPT_to_MODULE_EXPR
@@ -2034,7 +2033,7 @@ let rec xlate_vernac =
        xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
    | VernacInclude (_) -> xlate_error "TODO : Include "
-   | VernacDeclareModuleType((_, id), bl, mty_o)  ->
+   | VernacDeclareModuleType((_, id), bl, _, mty_o)  ->
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
@@ -2045,18 +2044,18 @@ let rec xlate_vernac =
 				CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
 				  (xlate_module_type mty1)
 	                    | _ -> failwith "TODO: Include Self")
-   | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
+   | VernacDefineModule(_,(_, id), bl, mtys, mexpr_o) ->
        CT_module(xlate_ident id,
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt mty_o,
+		 xlate_module_type_check mtys,
 		 match mexpr_o with
 		     [] -> 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) ->
+  | VernacDeclareModule(_,(_, id), bl, mty) ->
        CT_declare_module(xlate_ident id,
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt (Some mty_o),
+		 xlate_module_type_check (Topconstr.Enforce mty),
 		 CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
    | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 111f45ca7..afc5b9122 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -62,25 +62,25 @@ Module Type EqualityType := BareEquality <+ IsEq.
 
 Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig.
 
-Module Type EqualityTypeBoth (* <: EqualityType <: EqualityTypeOrig *)
+Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
  := BareEquality <+ IsEq <+ IsEqOrig.
 
-Module Type DecidableType (* <: EqualityType *)
+Module Type DecidableType <: EqualityType
  := BareEquality <+ IsEq <+ HasEqDec.
 
-Module Type DecidableTypeOrig (* <: EqualityTypeOrig *)
+Module Type DecidableTypeOrig <: EqualityTypeOrig
  := BareEquality <+ IsEqOrig <+ HasEqDec.
 
-Module Type DecidableTypeBoth (* <: DecidableType <: DecidableTypeOrig *)
+Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
  := EqualityTypeBoth <+ HasEqDec.
 
-Module Type BooleanEqualityType (* <: EqualityType *)
+Module Type BooleanEqualityType <: EqualityType
  := BareEquality <+ IsEq <+ HasEqBool.
 
-Module Type BooleanDecidableType (* <: DecidableType <: BooleanEqualityType *)
+Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
  := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool.
 
-Module Type DecidableTypeFull (* <: all previous interfaces *)
+Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
  := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
@@ -146,7 +146,7 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
    A particular case of [DecidableType] where the equality is
    the usual one of Coq. *)
 
-Module Type UsualBareEquality. (* <: BareEquality *)
+Module Type UsualBareEquality <: BareEquality.
  Parameter Inline t : Type.
  Definition eq := @eq t.
 End UsualBareEquality.
@@ -161,26 +161,22 @@ Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E.
  Definition eq_trans := @eq_trans E.t.
 End UsualIsEqOrig.
 
-Module Type UsualEqualityType (* <: EqualityType *)
+Module Type UsualEqualityType <: EqualityType
  := UsualBareEquality <+ IsEq.
 
-Module Type UsualDecidableType (* <: DecidableType *)
+Module Type UsualDecidableType <: DecidableType
  := UsualBareEquality <+ IsEq <+ HasEqDec.
 
-Module Type UsualDecidableTypeBoth (* <: DecidableTypeBoth *)
+Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
  := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec.
 
 Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool.
 
-Module Type UsualDecidableTypeFull (* <: DecidableTypeFull *)
+Module Type UsualDecidableTypeFull <: DecidableTypeFull
  := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
-(** a [UsualDecidableType] is in particular an [DecidableType]. *)
-
-Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
-
-(** Some shortcuts for easily building a UsualDecidableType *)
+(** Some shortcuts for easily building a [UsualDecidableType] *)
 
 Module Type MiniDecidableType.
  Parameter t : Type.
@@ -188,12 +184,9 @@ Module Type MiniDecidableType.
 End MiniDecidableType.
 
 Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
- Include M.
  Definition eq := @eq M.t.
- Include Self UsualIsEq.
- Include Self UsualIsEqOrig.
+ Include M <+ UsualIsEq <+ UsualIsEqOrig.
 End Make_UDT.
 
 Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
  := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
-
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 76e7eb0b8..4fcd717bb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -446,7 +446,7 @@ let vernac_import export refl =
     List.iter import refl;
     Lib.add_frozen_state ()
 
-let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
+let vernac_declare_module export (loc, id) binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
@@ -460,7 +460,7 @@ 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) []
+    id binders_ast (Enforce mty_ast) []
   in
     Dumpglob.dump_moddef loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is declared");
@@ -514,7 +514,7 @@ 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_l =
+let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections.";
 
@@ -526,7 +526,8 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_l =
          (fun (export,idl,ty) (args,argsexport) ->
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
-       let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
+       let mp = Declaremods.start_modtype
+	 Modintern.interp_modtype id binders_ast mty_sign in
         Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose message
 	  ("Interactive Module Type "^ string_of_id id ^" started");
@@ -545,7 +546,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_l =
 			"and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype
-	  id binders_ast mty_ast_l in
+	  id binders_ast mty_sign mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message
 	    ("Module Type "^ string_of_id id ^" is defined")
@@ -1329,10 +1330,10 @@ let interp c = match c with
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
       vernac_declare_module export lid bl mtyo
-  | 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
+  | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
+      vernac_define_module export lid bl mtys mexprl
+  | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
+      vernac_declare_module_type lid bl mtys mtyo
   | VernacInclude (is_self,in_asts) ->
       vernac_include is_self in_asts
   (* Gallina extensions *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ccb850651..6148b98ae 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -259,11 +259,11 @@ type vernac_expr =
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
-      module_binder list * (module_type_ast * bool)
+      module_binder list * module_type_ast
   | VernacDefineModule of bool option * lident *
-      module_binder list * (module_type_ast * bool) option * module_ast list
+      module_binder list * module_type_ast module_signature * module_ast list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_type_ast list
+      module_binder list * module_type_ast list * module_type_ast list
   | VernacInclude of bool * include_ast
 
   (* Solving *)