Variant !F M for functor application that does not honor the Inline declarations

 For F(X:T), the application !F M works as F M, except that if module type T
 contains some "Inline" annotations, they are not taken in account when substituting
 X with M in F. See forthcoming commits for examples of use for this feature.

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

13 files changed, 202 insertions, 162 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d93e1ab140..a20cd1bc23 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1009,6 +1009,8 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
+
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1b1698f956..3b5832f18c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -246,6 +246,8 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
+
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26ad7e383a..cfa256888e 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -224,12 +224,12 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and translate_module env mp me =
+and translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None ->
 	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
     | None, Some mte ->
-	let mtb = translate_module_type env mp mte in
+	let mtb = translate_module_type env mp inl mte in
 	  { mod_mp = mp;
 	    mod_expr = None;
 	    mod_type = mtb.typ_expr;
@@ -239,13 +239,13 @@ and translate_module env mp me =
 	    mod_retroknowledge = []}
    | Some mexpr, _ ->
 	let sign,alg_implem,resolver,cst1 =
-	  translate_struct_module_entry env mp mexpr in
+	  translate_struct_module_entry env mp inl mexpr in
 	let sign,alg1,resolver,cst2 =
 	  match me.mod_entry_type with
 	    | None ->
 		sign,None,resolver,Constraint.empty
 	    | Some mte ->
-		let mtb = translate_module_type env mp mte in
+		let mtb = translate_module_type env mp inl mte in
                 let cst = check_subtypes env
 		  {typ_mp = mp;
 		   typ_expr = sign;
@@ -269,21 +269,23 @@ and translate_module env mp me =
 	       fix the bug.*)
 
 
-and translate_struct_module_entry env mp mse  = match mse with
+and translate_struct_module_entry env mp inl mse  = match mse with
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in 
       let mb' = strengthen_and_subst_mb mb mp env false in
 	mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) arg_e in
+      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) 
 	env in
-      let sign,alg,resolver,cst = translate_struct_module_entry env' 
-	mp body_expr in
-	SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
+      let sign,alg,resolver,cst =
+	translate_struct_module_entry env' mp inl body_expr in
+      SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
       Univ.Constraint.union cst mtb.typ_constraints
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolver,cst1 = translate_struct_module_entry env mp fexpr in
+      let sign,alg,resolver,cst1 =
+	translate_struct_module_entry env mp inl fexpr
+      in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -294,32 +296,35 @@ and translate_struct_module_entry env mp mse  = match mse with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
-      let mp_delta =  discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1 
-	farg_id farg_b mp_delta in
+      let mp_delta = discr_resolver env mtb in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
       (subst_codom_delta_resolver subst resolver),
       Univ.Constraint.union cst1 cst
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp mte in
+      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
       let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
 	sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
 	  
-and translate_struct_type_entry env mse  = match mse with
+and translate_struct_type_entry env inl mse = match mse with
   | MSEident mp1 ->
       let mtb = lookup_modtype mp1 env in 
 	mtb.typ_expr,
       Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let mtb = translate_module_type env (MPbound arg_id) arg_e in
+      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env  in
-      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env' 
-	 body_expr in
+      let sign,alg,resolve,mp_from,cst =
+	translate_struct_type_entry env' inl body_expr in
 	SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
       Univ.Constraint.union cst mtb.typ_constraints
   | MSEapply (fexpr,mexpr) ->
-      let sign,alg,resolve,mp_from,cst1 = translate_struct_type_entry env fexpr in
+      let sign,alg,resolve,mp_from,cst1 =
+	translate_struct_type_entry env inl fexpr
+      in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -331,19 +336,20 @@ and translate_struct_type_entry env mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst2 = check_subtypes env mtb farg_b in
       let mp_delta = discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1
-	farg_id farg_b mp_delta in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),None,
       (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2
   | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in
+      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
       let sign,alg,resolve,cst1 = 
 	check_with env sign with_decl alg mp_from resolve in
 	sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1    
 
-and translate_module_type env mp mte =
-	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in
+and translate_module_type env mp inl mte =
+	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
 	 subst_modtype_and_resolver 
 	   {typ_mp = mp_from;
 	    typ_expr = sign;
@@ -351,14 +357,14 @@ and translate_module_type env mp mte =
 	    typ_constraints = cst;
 	    typ_delta = resolve} mp env
 	   
-let rec translate_struct_include_module_entry env mp mse  = match mse with
+let rec translate_struct_include_module_entry env mp inl mse  = match mse with
   | MSEident mp1 ->
       let mb = lookup_module mp1 env in 
       let mb' = strengthen_and_subst_mb mb mp env true in
 	mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty
   | MSEapply (fexpr,mexpr) ->
       let sign,resolver,cst1 =
-	translate_struct_include_module_entry env mp fexpr in
+	translate_struct_include_module_entry env mp inl fexpr in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mtb,mp1 = 
 	try
@@ -370,8 +376,9 @@ let rec translate_struct_include_module_entry env mp mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
       let mp_delta =  discr_resolver env mtb in
-      let mp_delta = complete_inline_delta_resolver env mp1 
-	farg_id farg_b mp_delta in
+      let mp_delta = if not inl then mp_delta else
+	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      in
       let subst = map_mbid farg_id mp1 mp_delta in
 	(subst_struct_expr subst fbody_b),
       (subst_codom_delta_resolver subst resolver),
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 746a80e151..63f7696c48 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -17,20 +17,20 @@ open Names
 (*i*)
 
 
-val translate_module : env -> module_path -> module_entry 
+val translate_module : env -> module_path -> bool -> module_entry
   -> module_body
 
-val translate_module_type : env -> module_path -> module_struct_entry -> 
+val translate_module_type : env -> module_path -> bool -> module_struct_entry ->
   module_type_body
 
-val translate_struct_module_entry : env -> module_path -> module_struct_entry -> 
+val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry ->
   struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
 
-val translate_struct_type_entry : env  -> module_struct_entry -> 
+val translate_struct_type_entry : env -> bool -> module_struct_entry ->
   struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints
 
 val translate_struct_include_module_entry : env -> module_path 
-  -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+  -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
 
 val add_modtype_constraints : env -> module_type_body -> env
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ef2ea800cf..e4c6ec35e1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,10 +262,10 @@ let add_mind dir l mie senv =
 
 (* Insertion of module types *)
 
-let add_modtype l mte senv =
+let add_modtype l mte inl senv =
   check_label l senv.labset;
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let mtb = translate_module_type senv.env mp mte  in
+  let mtb = translate_module_type senv.env mp inl mte  in
   let senv' = add_constraints mtb.typ_constraints senv in
    let env'' = Environ.add_modtype mp mtb senv'.env in
     mp, { old = senv'.old;
@@ -288,10 +288,10 @@ let full_add_module mb senv =
 
 (* Insertion of modules *)
 
-let add_module l me senv =
+let add_module l me inl senv =
   check_label l senv.labset;
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let mb = translate_module senv.env mp me in
+  let mb = translate_module senv.env mp inl me in
   let senv' = full_add_module mb senv  in
   let modinfo = match mb.mod_type with
       SEBstruct _ -> 
@@ -339,7 +339,9 @@ let end_module l restype senv =
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
   let mp = senv.modinfo.modpath in
-  let restype = Option.map (translate_module_type senv.env mp) restype in
+  let restype =
+    Option.map
+      (fun (res,inl) -> translate_module_type senv.env mp inl res) restype in
   let params,is_functor =
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -420,17 +422,17 @@ let end_module l restype senv =
 
 
 (* Include for module and module type*)
- let add_include me is_module senv =
+ let add_include me is_module inl senv =
    let sign,cst,resolver =
      if is_module then
        let sign,resolver,cst =  
 	 translate_struct_include_module_entry senv.env 
-	   senv.modinfo.modpath me in
+	   senv.modinfo.modpath inl me in
 	 sign,cst,resolver
      else
        let mtb = 
 	 translate_module_type senv.env 
-	   senv.modinfo.modpath me in
+	   senv.modinfo.modpath inl me in
        mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
    let senv = add_constraints cst senv in
@@ -441,8 +443,9 @@ let end_module l restype senv =
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
 	 let senv = add_constraints cst_sub senv in
-	 let mpsup_delta = complete_inline_delta_resolver senv.env mp_sup 
-	   mbid mtb mb.typ_delta in
+	 let mpsup_delta = if not inl then mb.typ_delta else
+	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta
+	 in
 	   (compute_sign 
 	     (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv)
      | str -> str,senv
@@ -534,10 +537,10 @@ let end_module l restype senv =
 
 (* Adding parameters to modules or module types *)
 
-let add_module_parameter mbid mte senv =
+let add_module_parameter mbid mte inl senv =
   if  senv.revstruct <> [] or senv.loads <> [] then
     anomaly "Cannot add a module parameter to a non empty module";
-  let mtb = translate_module_type senv.env (MPbound mbid) mte in
+  let mtb = translate_module_type senv.env (MPbound mbid) inl mte in
   let senv = 
     full_add_module (module_body_of_type (MPbound mbid) mtb) senv
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 169fd158d8..c378d8ccc7 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -55,12 +55,12 @@ val add_mind :
 
 (* Adding a module *)
 val add_module :
-  label -> module_entry -> safe_environment
+  label -> module_entry -> bool -> safe_environment
     -> module_path * delta_resolver * safe_environment
 
 (* Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> safe_environment
+  label -> module_struct_entry -> bool -> safe_environment
     -> module_path * safe_environment
 
 (* Adding universe constraints *)
@@ -76,11 +76,11 @@ val start_module :
   label -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> module_struct_entry option 
+  label -> (module_struct_entry * bool) option
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> safe_environment -> delta_resolver * safe_environment
+  mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
@@ -89,7 +89,7 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> bool -> safe_environment ->
+  module_struct_entry -> bool -> bool -> safe_environment ->
    delta_resolver * safe_environment
 
 val pack_module : safe_environment -> module_body
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5db0e0abc1..0092e29c52 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -79,8 +79,8 @@ let modtab_objects =
    is a functor) and declared output type *)
 let openmod_info =
   ref ((MPfile(initial_dir),[],None,[])
-	 : module_path *  mod_bound_id list * module_struct_entry option
-                                          * module_type_body list)
+	 : module_path *  mod_bound_id list *
+           (module_struct_entry * bool) option * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -147,22 +147,22 @@ let check_subtypes_mt mp sub_mtb_l =
 
 let funct_entry args m =
   List.fold_right
-    (fun (arg_id,arg_t) mte -> MSEfunctor (arg_id,arg_t,mte))
+    (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 ->
+    (fun (m,inl) ->
        let mte = interp_modtype (Global.env()) m in
-       let mtb = Mod_typing.translate_module_type (Global.env()) mp mte in
+       let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
        let funct_mtb =
 	 List.fold_right
-           (fun (arg_id,arg_t) mte ->
+           (fun (arg_id,(arg_t,arg_inl)) mte ->
               let arg_t =
 		Mod_typing.translate_module_type (Global.env())
-		  (MPbound arg_id) arg_t
+		  (MPbound arg_id) arg_inl arg_t
 	      in
               SEBfunctor(arg_id,arg_t,mte))
            args mtb.typ_expr
@@ -327,8 +327,8 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
     match entry with
       | None ->
 	  anomaly "You must not recache interactive module types!"
-      | Some mte ->
-	  if mp <> Global.add_modtype (basename sp) mte then
+      | Some (mte,inl) ->
+	  if mp <> Global.add_modtype (basename sp) mte inl then
 	    anomaly "Kernel and Library names do not match"
   in
 
@@ -428,38 +428,42 @@ let rec get_objs_modtype_application env = function
     Modops.error_application_to_not_path mexpr
 | _ -> error "Application of a non-functor."
 
-let rec compute_subst env mbids sign mp_l =
+let rec compute_subst env mbids sign mp_l inline =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
     | [],r -> error "Application of a functor with too few arguments."
     | mbid::mbids,mp::mp_l ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	let mb = Environ.lookup_module mp env in
-	let mbid_left,subst = compute_subst env mbids fbody_b mp_l in
+	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in
 	match discr_resolver mb with
 	  | None ->
 	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
 	  | Some mp_delta ->
-	      let mp_delta = Modops.complete_inline_delta_resolver env mp
-		farg_id farg_b mp_delta in
+	      let mp_delta =
+		if not inline then mp_delta else
+		  Modops.complete_inline_delta_resolver env mp
+		    farg_id farg_b mp_delta
+	      in
 	      mbid_left,join (map_mbid mbid mp mp_delta) subst
 
-let rec get_modtype_substobjs env mp_from= function
+let rec get_modtype_substobjs env mp_from inline = function
     MSEident ln -> 
       MPmap.find ln !modtypetab 
   | MSEfunctor (mbid,_,mte) ->
-      let (mbids, mp, objs) = get_modtype_substobjs env mp_from mte in
+      let (mbids, mp, objs) = get_modtype_substobjs env mp_from inline mte in
 	(mbid::mbids, mp, objs)
-  | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mp_from mty
+  | MSEwith (mty, With_Definition _) ->
+      get_modtype_substobjs env mp_from inline mty
   | MSEwith (mty, With_Module (idl,mp1)) -> 
-      let substobjs = get_modtype_substobjs env mp_from mty in
+      let substobjs = get_modtype_substobjs env mp_from inline mty in
       let modobjs = MPmap.find mp1 !modtab_substobjs in
 	replace_module_object idl substobjs modobjs mp1
   | MSEapply (fexpr, MSEident mp) as me ->
       let (mbids, mp1, objs),mtb_mp1,mp_l =
 	get_objs_modtype_application env me in
       let mbids_left,subst =
-	compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l)
+	compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) inline
       in
       (mbids_left, mp1,subst_objects subst objs)
   | MSEapply (_,mexpr) ->
@@ -468,41 +472,42 @@ let rec get_modtype_substobjs env mp_from= function
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
-  let process_arg id (mbid,mty) =
+  let process_arg id (mbid,(mty,inl)) =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
-    let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp mty in
-    let substobjs = (mbids,mp,subst_objects 
+    let (mbids,mp_from,objs) =
+      get_modtype_substobjs (Global.env()) mp inl mty in
+    let substobjs = (mbids,mp,subst_objects
 		       (map_mp mp_from mp empty_delta_resolver) objs)in
       do_module false "start" load_objects 1 dir mp substobjs []
     in
       List.iter2 process_arg argids args
-	
-let intern_args interp_modtype (idl,arg) =
+
+let intern_args interp_modtype (idl,(arg,inl)) =
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
   let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
-    (MPbound (List.hd mbids))  mty in
+    (MPbound (List.hd mbids)) inl mty in
   List.map2
     (fun dir mbid ->
-       let resolver = Global.add_module_parameter mbid mty in
+       let resolver = Global.add_module_parameter mbid mty inl in
        let mp = MPbound mbid in
-       let substobjs = (mbi,mp,subst_objects 
+       let substobjs = (mbi,mp,subst_objects
 			  (map_mp mp_from mp resolver) objs) in
 	 do_module false "interp" load_objects 1 dir mp substobjs [];
-	 (mbid,mty))
+	 (mbid,(mty,inl)))
     dirs mbids
 
 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_l = match res with
-    | Topconstr.Enforce res ->
+    | Topconstr.Enforce (res,inl) ->
 	let mte = interp_modtype (Global.env()) res in
-	let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in
-	Some mte, []
+	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
+	Some (mte,inl), []
     | Topconstr.Check resl ->
 	None, build_subtypes interp_modtype mp arg_entries resl
   in
@@ -524,16 +529,19 @@ let end_module () =
       | None ->
 	  (* the module is not sealed *)
 	  None,( mbids, mp, substitute), keep, special
-      | Some (MSEident ln as mty) ->
-	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+      | Some (MSEident ln as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
 	  Some mp1,(mbids@mbids1,mp1,objs), [], []
-      | Some (MSEwith _ as mty) ->
-	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+      | Some (MSEwith _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
 	  Some mp1,(mbids@mbids1,mp1,objs), [], []
-      | Some (MSEfunctor _) ->
+      | Some (MSEfunctor _, _) ->
 	  anomaly "Funsig cannot be here..."
-      | Some (MSEapply _ as mty) ->
-	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+      | Some (MSEapply _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
 	  Some mp1,(mbids@mbids1,mp1,objs), [], []
   with
 	Not_found -> anomaly "Module objects not found..."
@@ -690,13 +698,13 @@ let end_modtype () =
   mp
 
 
-let declare_modtype_ interp_modtype id args mtys mty fs =
+let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) 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
+  let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp inl entry in
   (* Undo the simulated interactive building of the module type *)
   (* and declare the module type as a whole *)
 
@@ -704,7 +712,7 @@ let declare_modtype_ interp_modtype id args mtys mty fs =
 		   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)));
+  ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
 
 
@@ -720,20 +728,20 @@ let rec get_objs_module_application env = function
 | _ -> error "Application of a non-functor."
 
 
-let rec get_module_substobjs env mp_from = function
+let rec get_module_substobjs env mp_from inl = function
   | MSEident mp -> MPmap.find mp !modtab_substobjs
   | MSEfunctor (mbid,mty,mexpr) ->
-       let (mbids, mp, objs) = get_module_substobjs env mp_from mexpr in
+       let (mbids, mp, objs) = get_module_substobjs env mp_from inl mexpr in
 	(mbid::mbids, mp, objs)
   | MSEapply (fexpr, MSEident mp) as me ->
       let (mbids, mp1, objs),mb_mp1,mp_l =
 	get_objs_module_application env me
       in
       let mbids_left,subst =
-	compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) in
+	compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in
       (mbids_left, mp1,subst_objects subst objs)
   | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
-  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty
+  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
   | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
 (* Include *)
@@ -816,13 +824,17 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
   let env = Global.env() in
-  let mty_entry_o, subs = match res with
-    | Topconstr.Enforce mty -> Some (funct interp_modtype mty), []
-    | Topconstr.Check mtys -> None, build_subtypes interp_modtype mmp arg_entries mtys
+  let mty_entry_o, subs, inl_res = match res with
+    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
+    | Topconstr.Check mtys ->
+	None, build_subtypes interp_modtype mmp arg_entries mtys, true
   in
  
   (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
-  let mexpr_entry_o = Option.map (funct interp_modexpr) mexpr_o in
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, true
+    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
+  in
   let entry =
     {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
@@ -830,8 +842,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   let substobjs =
     match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp mexpr
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
   let (mbids,mp_from,objs) = update_include substobjs in
@@ -839,7 +851,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   (* 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 mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in
 
   if mp_env <> mp then anomaly "Kernel and Library names do not match";
 
@@ -854,20 +866,21 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   mmp
 
 
-let rec include_subst env mb mbids sign =
+let rec include_subst env mb mbids sign inline =
   match mbids with
     | [] -> empty_subst
     | mbid::mbids ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
-	let subst = include_subst env mb mbids fbody_b in
-	let mp_delta =
+	let subst = include_subst env mb mbids fbody_b inline in
+	let mp_delta = if not inline then mb.mod_delta else
 	  Modops.complete_inline_delta_resolver env mb.mod_mp
-	    farg_id farg_b mb.mod_delta in
+	    farg_id farg_b mb.mod_delta
+	in
 	join (map_mbid mbid mb.mod_mp mp_delta) subst
 
 exception NothingToDo
 
-let get_includeself_substobjs env objs me is_mod =
+let get_includeself_substobjs env objs me is_mod inline =
   try
     let mb_mp = match me with
       | MSEident mp ->
@@ -893,32 +906,33 @@ let get_includeself_substobjs env objs me is_mod =
     in
     let (mbids,mp_self,objects) = objs in
     let mb = Global.pack_module() in
-    let subst = include_subst env mb mbids mb_mp.mod_type in
+    let subst = include_subst env mb mbids mb_mp.mod_type inline in
     ([],mp_self,subst_objects subst objects)
   with NothingToDo -> objs
 
-let declare_one_include_inner (me,is_mod) =
+let declare_one_include_inner inl (me,is_mod) =
   let env = Global.env() in
   let mp1,_ = current_prefix () in
   let (mbids,mp,objs)=
     if is_mod then
-      get_module_substobjs env mp1 me
+      get_module_substobjs env mp1 inl me
     else
-      get_modtype_substobjs env mp1 me in
+      get_modtype_substobjs env mp1 inl me in
   let (mbids,mp,objs) =
     if mbids <> [] then
-      get_includeself_substobjs env (mbids,mp,objs) me is_mod
+      get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
     else
       (mbids,mp,objs) in
   let id = current_mod_id() in
-  let resolver =  Global.add_include me is_mod in
+  let resolver =  Global.add_include me is_mod inl in
   let substobjs = (mbids,mp1,
 		   subst_objects (map_mp mp mp1 resolver) objs) in
   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)
+  declare_one_include_inner (snd me_ast)
+    (interp_struct (Global.env()) (fst me_ast))
 
 let declare_include_ interp_struct me_asts =
   List.iter (declare_one_include interp_struct) me_asts
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 1db3d95a88..e58f967441 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -41,13 +41,13 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   identifier ->
-  (identifier located list * 'modast) list ->
-  'modast Topconstr.module_signature ->
-  'modast list -> module_path
+  (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) Topconstr.module_signature ->
+  ('modast * bool) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
-  bool option -> identifier -> (identifier located list * 'modast) list ->
-  'modast Topconstr.module_signature -> module_path
+  bool option -> identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) Topconstr.module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -57,12 +57,12 @@ val end_module : unit -> 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
+  identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) list -> ('modast * bool) list -> module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  identifier -> (identifier located list * 'modast) list ->
-  'modast list -> module_path
+  identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) list -> module_path
 
 val end_modtype : unit -> module_path
 
@@ -106,7 +106,7 @@ val import_module : bool -> module_path -> unit
 (* Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
-  'struct_expr list -> unit
+  ('struct_expr * bool) list -> unit
 
 (*s [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented
@@ -122,5 +122,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 
 (* For translator *)
 val process_module_bindings : module_ident list ->
-  (mod_bound_id * module_struct_entry) list -> unit
+  (mod_bound_id * (module_struct_entry * bool)) list -> unit
 
diff --git a/library/global.ml b/library/global.ml
index 3129c1caf8..d5fafbb8bc 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -56,12 +56,12 @@ let add_thing add dir id thing =
 
 let add_constant = add_thing add_constant
 let add_mind = add_thing add_mind
-let add_modtype = add_thing (fun _ -> add_modtype) ()
+let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y
 
 
-let add_module id me =
+let add_module id me inl =
   let l = label_of_id id in
-  let mp,resolve,new_env = add_module l me !global_env in
+  let mp,resolve,new_env = add_module l me inl !global_env in
     global_env := new_env;
     mp,resolve
     
@@ -70,8 +70,8 @@ let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let add_include me is_module =
-  let resolve,newenv = add_include me is_module !global_env in
+let add_include me is_module inl =
+  let resolve,newenv = add_include me is_module inl !global_env in
     global_env := newenv;
     resolve
 
@@ -89,8 +89,8 @@ let end_module fs id mtyo =
     mp,resolve
 
 
-let add_module_parameter mbid mte =
-  let resolve,newenv = add_module_parameter mbid mte !global_env in
+let add_module_parameter mbid mte inl =
+  let resolve,newenv = add_module_parameter mbid mte inl !global_env in
     global_env := newenv;
     resolve
 
diff --git a/library/global.mli b/library/global.mli
index b7e7889125..a8d76c4f42 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -50,10 +50,12 @@ val add_constant :
 val add_mind        :
   dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
 
-val add_module      : identifier -> module_entry -> module_path * delta_resolver
-val add_modtype     : identifier -> module_struct_entry -> module_path
+val add_module      :
+ identifier -> module_entry -> bool -> module_path * delta_resolver
+val add_modtype     :
+ identifier -> module_struct_entry -> bool -> module_path
 val add_include :
- module_struct_entry -> bool -> delta_resolver
+ module_struct_entry -> bool -> bool -> delta_resolver
 
 val add_constraints : constraints -> unit
 
@@ -68,10 +70,11 @@ val set_engagement : engagement -> unit
 
 val start_module : identifier -> module_path
 
-val end_module : Summary.frozen ->identifier -> module_struct_entry option -> 
-  module_path * delta_resolver
+val end_module : Summary.frozen ->identifier ->
+  (module_struct_entry * bool) option -> module_path * delta_resolver
 
-val add_module_parameter : mod_bound_id -> module_struct_entry -> delta_resolver
+val add_module_parameter :
+ mod_bound_id -> module_struct_entry -> bool -> delta_resolver
 
 val start_modtype : identifier -> module_path
 val end_modtype : Summary.frozen -> identifier -> module_path
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f4d588b572..f0d90b11b8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -380,7 +380,7 @@ GEXTEND Gram
 	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 ->
+	bl = LIST0 module_binder; ":"; mty = module_type_inl ->
 	  VernacDeclareModule (export, id, bl, mty)
       (* Section beginning *)
       | IDENT "Section"; id = identref -> VernacBeginSection id
@@ -396,9 +396,9 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | 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 ->
+      | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
-      | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type ->
+      | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  warning "Include Type is deprecated; use Include instead";
           VernacInclude(e::l) ] ]
   ;
@@ -408,36 +408,42 @@ GEXTEND Gram
       |  -> None ] ]
   ;
   ext_module_type:
-    [ [ "<+"; mty = module_type -> mty ] ]
+    [ [ "<+"; mty = module_type_inl -> mty ] ]
   ;
   ext_module_expr:
-    [ [ "<+"; mexpr = module_expr -> mexpr ] ]
+    [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ]
   ;
   check_module_type:
-    [ [ "<:"; mty = module_type -> mty ] ]
+    [ [ "<:"; mty = module_type_inl -> mty ] ]
   ;
   check_module_types:
     [ [ mtys = LIST0 check_module_type -> mtys ] ]
   ;
   of_module_type:
-    [ [ ":"; mty = module_type -> Enforce mty
+    [ [ ":"; mty = module_type_inl -> Enforce mty
       | mtys = check_module_types -> Check mtys ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l)
+    [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l)
       | -> [] ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l)
+    [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l)
       | -> [] ] ]
   ;
-
+  module_expr_inl:
+    [ [ "!"; me = module_expr -> (me,false)
+      | me = module_expr -> (me,true) ] ]
+  ;
+  module_type_inl:
+    [ [ "!"; me = module_type -> (me,false)
+      | me = module_type -> (me,true) ] ]
+  ;
   (* Module binder  *)
   module_binder:
     [ [ "("; export = export_token; idl = LIST1 identref; ":";
-         mty = module_type; ")" -> (export,idl,mty) ] ]
+         mty = module_type_inl; ")" -> (export,idl,mty) ] ]
   ;
-
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 92a455abce..6d3cf76b27 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -246,24 +246,27 @@ let rec pr_module_ast pr_c = function
       pr_module_ast pr_c me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
 
+let pr_module_ast_inl pr_c (mast,b) =
+  (if b then mt () else str "!") ++ pr_module_ast pr_c mast
+
 let pr_of_module_type prc = function
-  | Enforce mty -> str ":" ++ pr_module_ast prc mty
+  | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
   | Check mtys ->
-      prlist_strict (fun m -> str "<:" ++ pr_module_ast prc m) mtys
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl prc m) mtys
 
 let pr_require_token = function
   | Some true -> str "Export "
   | Some false -> str "Import "
   | None -> mt()
 
-let pr_module_vardecls pr_c (export,idl,mty) =
+let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
   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) ->
     Declaremods.process_module_bindings [id]
       [make_mbid lib_dir (string_of_id id),
-       Modintern.interp_modtype (Global.env()) mty]) idl;
+       (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
   (* Builds the stream *)
   spc() ++
   hov 1 (str"(" ++ pr_require_token export ++
@@ -745,21 +748,21 @@ let rec pr_vernac = function
                pr_of_module_type pr_lconstr tys ++
 	       (if bd = [] then mt () else str ":= ") ++
 	       prlist_with_sep (fun () -> str " <+ ")
-	        (pr_module_ast pr_lconstr) bd)
+	        (pr_module_ast_inl 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_ast pr_lconstr m1)
+             pr_module_ast_inl pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,tyl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in
-      let pr_mt = pr_module_ast pr_lconstr in
+      let pr_mt = pr_module_ast_inl 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 (mexprs) ->
-      let pr_m = pr_module_ast pr_lconstr in
+      let pr_m = pr_module_ast_inl pr_lconstr in
       hov 2 (str"Include " ++
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d95fdbec95..8e5f2d8fce 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_ast
+type module_binder = bool option * lident list * module_ast_inl
 
 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_ast
+      module_binder list * module_ast_inl
   | VernacDefineModule of bool option * lident *
-      module_binder list * module_ast module_signature * module_ast list
+      module_binder list * module_ast_inl module_signature * module_ast_inl list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_ast list * module_ast list
-  | VernacInclude of module_ast list
+      module_binder list * module_ast_inl list * module_ast_inl list
+  | VernacInclude of module_ast_inl list
 
   (* Solving *)