A fine-grain control of inlining at functor application via priority levels

  As said in CHANGES:

<<
  The inlining done during application of functors can now be controlled
  more precisely. In addition to the "!F G" syntax preventing any inlining,
  we can now use a priority level to select parameters to inline :
  "<30>F G" means "only inline in F the parameters whose levels are <= 30".
  The level of a parameter can be fixed by "Parameter Inline(30) foo".
  When levels aren't given, the default value is 100. One can also use
  the flag "Set Inline Level ..." to set a level.
>>

  Nota : the syntax "Parameter Inline(30) foo" is equivalent to
  "Set Inline Level 30. Parameter Inline foo.",
  and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."

  For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
  while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
  We could achieve this behavior by setting a level such as 30 to the
  parameter eq, and then tweaking the current level when applying functors.

  This idea of levels might be too restrictive, we'll see, but at least
  the implementation of this change was quite simple. There might be
  situation where parameters cannot be linearly ordered according to their
  "inlinablility". For these cases, we would need to mention names to inline
  or not at a functor application, and this is a bit more tricky
  (and might be a pain to use if there are many names).

  No documentation for the moment, since this feature is experimental
  and might still evolve.

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

40 files changed, 218 insertions, 160 deletions

diff --git a/CHANGES b/CHANGES
index aa0357fbb..d885f604a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,16 @@ Vernacular commands
 - The undocumented and obsolete option "Set/Unset Boxed Definitions" has
   been removed, as well as syntaxes like "Boxed Fixpoint foo".
 
+Module System
+
+- The inlining done during application of functors can now be controlled
+  more precisely. In addition to the "!F G" syntax preventing any inlining,
+  we can now use a priority level to select parameters to inline :
+  "<30>F X" means "only inline in F the parameters whose levels are <= 30".
+  The level of a parameter can be fixed by "Parameter Inline(30) foo".
+  When levels aren't given, the default value is 100. One can also use
+  the flag "Set Inline Level ..." to set a level. TODO: DOC!
+
 Libraries
 
 - Creation of PArith, a subdirectory containing files about the positive type,
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 664712dd5..190e14eb1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -553,6 +553,8 @@ let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -561,7 +563,7 @@ type constant_body = {
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : Univ.constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 let val_cb = val_tuple ~name:"constant_body"
   [|val_nctxt;
diff --git a/checker/declarations.mli b/checker/declarations.mli
index ee44c8d5f..b5038996c 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -29,6 +29,8 @@ type constr_substituted
 val force_constr : constr_substituted -> constr
 val from_val : constr -> constr_substituted
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -36,7 +38,7 @@ type constant_body = {
     const_body_code : to_patch_substituted;
     const_constraints : Univ.constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 (* Mutual inductives *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f8c0aeb87..81b4e8e94 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1218,7 +1218,12 @@ 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 *)
+(* Which inline annotations should we honor, either None or the ones
+   whose level is less or equal to the given integer *)
+
+type inline = int option
+
+type module_ast_inl = module_ast * inline
 
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 405db2d17..b7bac17bd 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -264,7 +264,12 @@ 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 *)
+(* Which inline annotations should we honor, either None or the ones
+   whose level is less or equal to the given integer *)
+
+type inline = int option
+
+type module_ast_inl = module_ast * inline
 
 type 'a module_signature =
   | Enforce of 'a (** ... : T *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d01398841..87474b863 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -137,4 +137,4 @@ let cook_constant env r =
 	let j = make_judge (force (Option.get body)) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  (body, typ, cb.const_constraints, cb.const_opaque, false)
+  (body, typ, cb.const_constraints, cb.const_opaque, None)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 09b42d0b1..4b8b4537c 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type recipe = {
 
 val cook_constant :
   env -> recipe ->
-    constr_substituted option * constant_type * constraints * bool * bool
+    constr_substituted option * constant_type * constraints * bool * inline
 
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4308f9c1a..282dad0da 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,6 +49,8 @@ let force = force subst_mps
 
 let subst_constr_subst = subst_substituted
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -57,7 +59,7 @@ type constant_body = {
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 (*s Inductive types (internal representation with redundant
     information). *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index a92cb2cb4..d4c86fb35 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -35,6 +35,8 @@ type constr_substituted
 val from_val : constr -> constr_substituted
 val force : constr_substituted -> constr
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -43,7 +45,7 @@ type constant_body = {
    (* const_type_code : to_patch;*)
     const_constraints : constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index dbf802bb1..28f11c9af 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -59,8 +59,9 @@ type definition_entry = {
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
-(* type and the inlining flag *)
-type parameter_entry = types * bool
+type inline = int option (* inlining level, None for no inlining *)
+
+type parameter_entry = types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/entries.mli b/kernel/entries.mli
index d45e2bbdb..08740afae 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -55,7 +55,9 @@ type definition_entry = {
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
-type parameter_entry = types * bool  (*inline flag*)
+type inline = int option (* inlining level, None for no inlining *)
+
+type parameter_entry = types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 452c2e69a..9e8ce3fe5 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -18,9 +18,11 @@ open Util
 open Names
 open Term
 
+(* For Inline, the int is an inlining level, and the constr (if present)
+   is the term into which we should inline *)
 
 type delta_hint =
-    Inline of constr option
+    Inline of int * constr option
   | Equiv of kernel_name
   | Prefix_equiv of module_path
 
@@ -63,11 +65,11 @@ let add_mp mp1 mp2 resolve =
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
 let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
 
-let add_inline_delta_resolver con =
-  Deltamap.add (KN(user_con con)) (Inline None)
-    
-let add_inline_constr_delta_resolver con cstr =
-  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
+let add_inline_delta_resolver con lev =
+  Deltamap.add (KN(user_con con)) (Inline (lev,None))
+
+let add_inline_constr_delta_resolver con lev cstr =
+  Deltamap.add (KN(user_con con)) (Inline (lev, Some cstr))
 
 let add_constant_delta_resolver con =
   Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
@@ -131,15 +133,15 @@ let rec find_prefix resolve mp =
     with
 	Not_found -> mp
 
-exception Change_equiv_to_inline of constr
+exception Change_equiv_to_inline of (int * constr)
 
 let solve_delta_kn resolve kn =
   try 
       match Deltamap.find (KN kn) resolve with
 	| Equiv kn1 -> kn1
-	| Inline (Some c) -> 
-	    raise (Change_equiv_to_inline c)
-	| Inline None -> raise Inline_kn
+	| Inline (lev, Some c) ->
+	    raise (Change_equiv_to_inline (lev,c))
+	| Inline (_, None) -> raise Inline_kn
 	| _ -> anomaly 
 	    "mod_subst: bad association in delta_resolver"
   with
@@ -199,13 +201,16 @@ let mind_of_delta2 resolve mind =
 	_ -> mind
 	  
 
-let inline_of_delta resolver = 
-  let extract key hint l =
-    match key,hint with 
-      |KN kn, Inline _ -> kn::l
-      | _,_ -> l
-  in
-    Deltamap.fold extract resolver []
+let inline_of_delta inline resolver =
+  match inline with
+    | None -> []
+    | Some inl_lev ->
+      let extract key hint l =
+	match key,hint with
+	  |KN kn, Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l
+	  | _,_ -> l
+      in
+      Deltamap.fold extract resolver []
 
 exception Not_inline
   
@@ -213,14 +218,12 @@ let constant_of_delta_with_inline resolve con =
   let kn1,kn2 = canonical_con con,user_con con in
     try
       match Deltamap.find (KN kn2) resolve with 
-	| Inline None -> None
-	| Inline (Some const) -> Some const
+	| Inline (_,o) -> o
 	| _ -> raise Not_inline
     with
 	Not_found | Not_inline -> 
 	  try match Deltamap.find (KN kn1) resolve with 
-	    | Inline None -> None
-	    | Inline (Some const) -> Some const
+	    | Inline (_,o) -> o
 	    | _ -> raise Not_inline
 	  with
 	      Not_found | Not_inline -> None
@@ -575,12 +578,12 @@ let subst_codom_delta_resolver subst resolver =
 	  (try
 	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
 	   with
-	       Change_equiv_to_inline c ->
-		 Deltamap.add key (Inline (Some c)) resolver)
-      | Inline None ->
+	       Change_equiv_to_inline (lev,c) ->
+		 Deltamap.add key (Inline (lev,Some c)) resolver)
+      | Inline (_,None) ->
 	  Deltamap.add key hint resolver
-      | Inline (Some t) ->
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      | Inline (lev,Some t) ->
+	  Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver
   in
     Deltamap.fold apply_subst resolver empty_delta_resolver
 
@@ -597,14 +600,14 @@ let subst_dom_codom_delta_resolver subst resolver =
 	    (try
 	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
 	     with
-		 Change_equiv_to_inline c ->
-		   Deltamap.add key (Inline (Some c)) resolver)
-      | (KN kn),Inline None ->
+		 Change_equiv_to_inline (lev,c) ->
+		   Deltamap.add key (Inline (lev,Some c)) resolver)
+      | (KN kn),Inline (_,None) ->
 	  let key = KN (subst_kn subst kn) in
 	    Deltamap.add key hint resolver
-      | (KN kn),Inline (Some t) ->
+      | (KN kn),Inline (lev,Some t) ->
 	  let key = KN (subst_kn subst kn) in
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+	  Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver
       | _,_ -> anomaly "Mod_subst: Bad association in resolver" 
   in
     Deltamap.fold apply_subst resolver empty_delta_resolver
@@ -625,8 +628,8 @@ let update_delta_resolver resolver1 resolver2 =
 		   Equiv (solve_delta_kn resolver2 kn)
 		 in Deltamap.add key new_hint res
 	       with
-		   Change_equiv_to_inline c ->
-		     Deltamap.add key (Inline (Some c)) res)
+		   Change_equiv_to_inline (lev,c) ->
+		     Deltamap.add key (Inline (lev,Some c)) res)
 	  | _ -> Deltamap.add key hint res
       with Not_found ->
 	Deltamap.add key hint res
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 7164d1162..91139985b 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -19,10 +19,11 @@ type substitution
 
 val empty_delta_resolver : delta_resolver
 
-val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver
+val add_inline_delta_resolver :
+  constant -> int -> delta_resolver -> delta_resolver
 
-val add_inline_constr_delta_resolver :  constant -> constr -> delta_resolver 
-  -> delta_resolver
+val add_inline_constr_delta_resolver :
+  constant -> int -> constr -> delta_resolver -> delta_resolver
 
 val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
 
@@ -50,7 +51,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 val delta_of_mp : delta_resolver -> module_path -> module_path
 
 (** Extract the set of inlined constant in the resolver *)
-val inline_of_delta : delta_resolver -> kernel_name list
+val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
 
 (** remove_mp is used for the computation of a resolver induced by Include P *)
 val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 407ae73ca..13ac21437 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -294,11 +294,11 @@ and translate_struct_module_entry env mp inl 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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl 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),
+      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.union_constraints cst1 cst
   | MSEwith(mte, with_decl) ->
@@ -333,12 +333,13 @@ and translate_struct_type_entry env inl 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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta
+      in
+      let subst = map_mbid farg_id mp1 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.union_constraints cst1 cst2
+      (subst_struct_expr subst fbody_b),None,
+      (subst_codom_delta_resolver subst resolve),mp_from,
+      Univ.union_constraints cst1 cst2
   | MSEwith(mte, with_decl) ->
       let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
       let sign,alg,resolve,cst1 = 
@@ -375,11 +376,11 @@ let rec translate_struct_include_module_entry env mp inl 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 = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta
+      in
+      let subst = map_mbid farg_id mp1 mp_delta
       in
-      let subst = map_mbid farg_id mp1 mp_delta in
-	(subst_struct_expr subst fbody_b),
+      (subst_struct_expr subst fbody_b),
       (subst_codom_delta_resolver subst resolver),
       Univ.union_constraints cst1 cst
   | _ -> error ("You cannot Include a high-order structure.")
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index f14d63be9..81974edfa 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -13,20 +13,20 @@ open Mod_subst
 open Names
 
 
-val translate_module : env -> module_path -> bool -> module_entry
+val translate_module : env -> module_path -> inline -> module_entry
   -> module_body
 
-val translate_module_type : env -> module_path -> bool -> module_struct_entry ->
+val translate_module_type : env -> module_path -> inline -> module_struct_entry ->
   module_type_body
 
-val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry ->
+val translate_struct_module_entry : env -> module_path -> inline -> module_struct_entry ->
   struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
 
-val translate_struct_type_entry : env -> bool -> module_struct_entry ->
+val translate_struct_type_entry : env -> inline -> 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 
-  -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+val translate_struct_include_module_entry : env -> module_path -> inline ->
+  module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
 
 val add_modtype_constraints : env -> module_type_body -> env
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index ce968b40e..2bcfada96 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -364,31 +364,28 @@ let module_type_of_module env mp mb =
 	 typ_constraints = mb.mod_constraints;
 	 typ_delta = mb.mod_delta}
 
-let complete_inline_delta_resolver env mp mbid mtb delta =
-  let constants = inline_of_delta mtb.typ_delta in
+let inline_delta_resolver env inl mp mbid mtb delta =
+  let constants = inline_of_delta inl mtb.typ_delta in
   let rec make_inline delta = function
     | [] -> delta
-    | kn::r -> 
+    | (lev,kn)::r ->
 	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
 	let con = constant_of_kn kn in
 	let con' = constant_of_delta delta con in
-	  try
-	    let constant = lookup_constant con' env in
-	      if (not constant.Declarations.const_opaque) then
-		let constr = Option.map Declarations.force 
-		  constant.Declarations.const_body in
-		  if constr = None then 
-		    (make_inline delta r)
-		  else
-		    add_inline_constr_delta_resolver con (Option.get constr)
-		      (make_inline delta r)
-	      else
-		(make_inline delta r)
-	  with 
-	      Not_found -> error_no_such_label_sub (con_label con) 
-		(string_of_mp (con_modpath con))
+	try
+	  let constant = lookup_constant con' env in
+	  let l = make_inline delta r in
+	  if constant.Declarations.const_opaque then l
+	  else match constant.Declarations.const_body with
+	    | None -> l
+	    | Some body ->
+	      let constr = Declarations.force body in
+	      add_inline_constr_delta_resolver con lev constr l
+	with Not_found ->
+	  error_no_such_label_sub (con_label con)
+	    (string_of_mp (con_modpath con))
   in
-    make_inline delta constants
+  make_inline delta constants
 
 let rec strengthen_and_subst_mod
     mb subst env mp_from mp_to env resolver =
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 9c00b8194..f34fa88c4 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -39,8 +39,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit
 
 val strengthen : env -> module_type_body -> module_path -> module_type_body
 
-val complete_inline_delta_resolver :
-  env -> module_path -> mod_bound_id -> module_type_body ->
+val inline_delta_resolver :
+  env -> inline -> module_path -> mod_bound_id -> module_type_body ->
   delta_resolver -> delta_resolver
 
 val strengthen_and_subst_mb : module_body -> module_path -> env -> bool 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2bed2bb48..41ec0c6a6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,11 +262,9 @@ let add_constant dir l decl senv =
   in
   let senv' = add_constraints cb.const_constraints senv in
   let env'' = Environ.add_constant kn cb senv'.env in
-  let resolver = 
-    if cb.const_inline then
-      add_inline_delta_resolver kn senv'.modinfo.resolver
-    else
-      senv'.modinfo.resolver
+  let resolver = match cb.const_inline with
+    | None -> senv'.modinfo.resolver
+    | Some lev -> add_inline_delta_resolver kn lev senv'.modinfo.resolver
   in
     kn, { old = senv'.old;
 	  env = env'';
@@ -492,8 +490,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 = if not inl then mb.typ_delta else
-	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta in
+	 let mpsup_delta =
+	   inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
+	 in
 	 let subst = map_mbid mbid mp_sup mpsup_delta in
 	 let resolver = subst_codom_delta_resolver subst resolver in
 	   (compute_sign 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 406727664..0ab70b69e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -53,12 +53,12 @@ val add_mind :
 
 (** Adding a module *)
 val add_module :
-  label -> module_entry -> bool -> safe_environment
+  label -> module_entry -> inline -> safe_environment
     -> module_path * delta_resolver * safe_environment
 
 (** Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> bool -> safe_environment
+  label -> module_struct_entry -> inline -> safe_environment
     -> module_path * safe_environment
 
 (** Adding universe constraints *)
@@ -75,11 +75,11 @@ val start_module :
   label -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> (module_struct_entry * bool) option
+  label -> (module_struct_entry * inline) option
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
+  mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
@@ -88,7 +88,7 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> bool -> bool -> safe_environment ->
+  module_struct_entry -> bool -> inline -> safe_environment ->
    delta_resolver * safe_environment
 
 val pack_module : safe_environment -> module_body
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 432460d7d..801bd6c80 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -94,7 +94,7 @@ let infer_declaration env dcl =
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       Some (Declarations.from_val j.uj_val), typ, cst,
-        c.const_entry_opaque, false
+        c.const_entry_opaque, None
   | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
       None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 500858a59..8b48fc3cf 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-   constr_substituted option * constant_type * constraints * bool * bool
+   constr_substituted option * constant_type * constraints * bool * inline
 
 val build_constant_declaration : env -> 'a ->
-    constr_substituted option * constant_type * constraints * bool * bool ->
+    constr_substituted option * constant_type * constraints * bool * inline ->
       constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body
diff --git a/lib/flags.ml b/lib/flags.ml
index 13f540379..6d1fb7fae 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -124,3 +124,9 @@ let camlbin = ref Coq_config.camlbin
 let camlp4bin_spec = ref false
 let camlp4bin = ref Coq_config.camlp4bin
 
+(* Level of inlining during a functor application *)
+
+let default_inline_level = 100
+let inline_level = ref default_inline_level
+let set_inline_level = (:=) inline_level
+let get_inline_level () = !inline_level
diff --git a/lib/flags.mli b/lib/flags.mli
index ecb4d6dd6..20e3a7819 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -84,3 +84,8 @@ val camlbin_spec : bool ref
 val camlbin : string ref
 val camlp4bin_spec : bool ref
 val camlp4bin : string ref
+
+(** Level of inlining during a functor application *)
+val set_inline_level : int -> unit
+val get_inline_level : unit -> int
+val default_inline_level : int
diff --git a/library/declare.ml b/library/declare.ml
index fa95fe313..c566cedfd 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -139,7 +139,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
+let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,None))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 58b0d6a46..b6b3a766f 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -78,7 +78,7 @@ let modtab_objects =
 let openmod_info =
   ref ((MPfile(initial_dir),[],None,[])
 	 : module_path *  mod_bound_id list *
-           (module_struct_entry * bool) option * module_type_body list)
+           (module_struct_entry * inline) option * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -425,24 +425,20 @@ 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 inline =
+let rec compute_subst env mbids sign mp_l inl =
   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 inline in
-	match discr_resolver mb with
-	  | None ->
-	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
+	let resolver = match discr_resolver mb with
+	  | None -> empty_delta_resolver
 	  | Some mp_delta ->
-	      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
+	      Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta
+	in
+	mbid_left,join (map_mbid mbid mp resolver) subst
 
 let rec get_modtype_substobjs env mp_from inline = function
     MSEident ln -> 
@@ -748,15 +744,16 @@ 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 default_inl = Some (Flags.get_inline_level ()) in (* PLTODO *)
   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
+	None, build_subtypes interp_modtype mmp arg_entries mtys, default_inl
   in
  
   (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
   let mexpr_entry_o, inl_expr = match mexpr_o with
-    | None -> None, true
+    | None -> None, default_inl
     | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
   in
   let entry =
@@ -775,7 +772,8 @@ 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 (inl_expr&&inl_res) in
+  let inl = if inl_expr = None then None else inl_res in (*PLTODO *)
+  let mp_env,resolver = Global.add_module id entry inl in
 
   if mp_env <> mp then anomaly "Kernel and Library names do not match";
 
@@ -853,8 +851,8 @@ let rec include_subst env mb mbids sign inline =
     | mbid::mbids ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	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
+	let mp_delta =
+	  Modops.inline_delta_resolver env inline mb.mod_mp
 	    farg_id farg_b mb.mod_delta
 	in
 	join (map_mbid mbid mb.mod_mp mp_delta) subst
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 83c6b2bb6..b1978c282 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -37,13 +37,13 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   identifier ->
-  (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) Topconstr.module_signature ->
-  ('modast * bool) list -> module_path
+  (identifier located list * ('modast * inline)) list ->
+  ('modast * inline) Topconstr.module_signature ->
+  ('modast * inline) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
-  bool option -> identifier -> (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) Topconstr.module_signature -> module_path
+  bool option -> identifier -> (identifier located list * ('modast * inline)) list ->
+  ('modast * inline) Topconstr.module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -53,12 +53,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 * bool)) list ->
-  ('modast * bool) list -> ('modast * bool) list -> module_path
+  identifier -> (identifier located list * ('modast * inline)) list ->
+  ('modast * inline) list -> ('modast * inline) list -> module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  identifier -> (identifier located list * ('modast * bool)) list ->
-  ('modast * bool) list -> module_path
+  identifier -> (identifier located list * ('modast * inline)) list ->
+  ('modast * inline) list -> module_path
 
 val end_modtype : unit -> module_path
 
@@ -103,7 +103,7 @@ val import_module : bool -> module_path -> unit
 (** Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
-  ('struct_expr * bool) list -> unit
+  ('struct_expr * inline) list -> unit
 
 (** {6 ... } *)
 (** [iter_all_segments] iterate over all segments, the modules'
@@ -120,5 +120,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 
 (** For translator *)
 val process_module_bindings : module_ident list ->
-  (mod_bound_id * (module_struct_entry * bool)) list -> unit
+  (mod_bound_id * (module_struct_entry * inline)) list -> unit
 
diff --git a/library/global.mli b/library/global.mli
index eb58fd86e..9beb535d5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -48,11 +48,11 @@ val add_mind        :
   dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
 
 val add_module      :
- identifier -> module_entry -> bool -> module_path * delta_resolver
+ identifier -> module_entry -> inline -> module_path * delta_resolver
 val add_modtype     :
- identifier -> module_struct_entry -> bool -> module_path
+ identifier -> module_struct_entry -> inline -> module_path
 val add_include :
- module_struct_entry -> bool -> bool -> delta_resolver
+ module_struct_entry -> bool -> inline -> delta_resolver
 
 val add_constraints : constraints -> unit
 
@@ -68,10 +68,10 @@ val set_engagement : engagement -> unit
 val start_module : identifier -> module_path
 
 val end_module : Summary.frozen ->identifier ->
-  (module_struct_entry * bool) option -> module_path * delta_resolver
+  (module_struct_entry * inline) option -> module_path * delta_resolver
 
 val add_module_parameter :
- mod_bound_id -> module_struct_entry -> bool -> delta_resolver
+ mod_bound_id -> module_struct_entry -> inline -> 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 f6943871c..0c7dbeeb0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -215,7 +215,9 @@ GEXTEND Gram
       | IDENT "Parameters" -> (Global, Definitional) ] ]
   ;
   inline:
-    [ ["Inline" -> true |  -> false] ]
+    [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i)
+      | IDENT "Inline" -> Some (Flags.get_inline_level())
+      | -> None] ]
   ;
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)
@@ -443,12 +445,14 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   module_expr_inl:
-    [ [ "!"; me = module_expr -> (me,false)
-      | me = module_expr -> (me,true) ] ]
+    [ [ "!"; me = module_expr -> (me,None)
+      | "<"; i = INT; ">"; me = module_expr -> (me,Some (int_of_string i))
+      | me = module_expr -> (me,Some (Flags.get_inline_level())) ] ]
   ;
   module_type_inl:
-    [ [ "!"; me = module_type -> (me,false)
-      | me = module_type -> (me,true) ] ]
+    [ [ "!"; me = module_type -> (me,None)
+      | "<"; i = INT; ">"; me = module_type -> (me,Some (int_of_string i))
+      | me = module_type -> (me,Some (Flags.get_inline_level())) ] ]
   ;
   (* Module binder  *)
   module_binder:
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 21281f6e4..42007e4b0 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -227,8 +227,8 @@ 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_module_ast_inl pr_c (mast,o) =
+  (if o=None then str "!" else mt ()) ++ pr_module_ast pr_c mast
 
 let pr_of_module_type prc = function
   | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 30c88602d..1218dd80c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -153,7 +153,8 @@ let rec seb2mse = function
 
 let expand_seb env mp seb =
   let seb,_,_,_ =
-    Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+    let inl = Some (Flags.get_inline_level()) in
+    Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb)
   in seb
 
 (** When possible, we use the nicer, shorter, algebraic type structures
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 3d1e836a7..e8e1fc25f 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -603,7 +603,7 @@ let admit_obligations n =
 	match x.obl_body with
 	| None ->
             let x = subst_deps_obl obls x in
-	    let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), 
+	    let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None),
 							 IsAssumption Conjectural) 
 	    in
 	      assumption_message x.obl_name;
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index a6a36672b..9e017bbd8 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1410,7 +1410,7 @@ let add_morphism_infer glob m n =
   let instance = build_morphism_signature m in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
-				(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+				(Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11bb6b436..ab04ebaf6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3417,7 +3417,7 @@ let admit_as_an_axiom gl =
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
   if occur_existential concl then error"\"admit\" cannot handle existentials.";
   let axiom =
-    let cd = Entries.ParameterEntry (concl,false) in
+    let cd = Entries.ParameterEntry (concl,None) in
     let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in
     constr_of_global (ConstRef con)
   in
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 8d56772ac..4dedcfe32 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -18,7 +18,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax.
 *)
 
 Module Type ZeroSuccPred (Import T:Typ).
- Parameter Inline zero : t.
+ Parameter Inline(20) zero : t.
  Parameters Inline succ pred : t -> t.
 End ZeroSuccPred.
 
@@ -47,7 +47,7 @@ End IsNZDomain.
 *)
 
 Module Type OneTwo (Import T:Typ).
- Parameter Inline one two : t.
+ Parameter Inline(20) one two : t.
 End OneTwo.
 
 Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T).
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 8e72bd611..2fbdff624 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -21,13 +21,13 @@ End Nop.
 (** * Structure with just a base type [t] *)
 
 Module Type Typ.
-  Parameter Inline t : Type.
+  Parameter Inline(10) t : Type.
 End Typ.
 
 (** * Structure with an equality relation [eq] *)
 
 Module Type HasEq (Import T:Typ).
-  Parameter Inline eq : t -> t -> Prop.
+  Parameter Inline(30) eq : t -> t -> Prop.
 End HasEq.
 
 Module Type Eq := Typ <+ HasEq.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f11bdb4a8..9b6c74398 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -179,7 +179,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	  (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None false imps ?hook (ConstRef cst); id
       end
     else
@@ -286,7 +286,7 @@ let context ?(hook=fun _ -> ()) l =
   let fn (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	(ParameterEntry (t,false), IsAssumption Logical)
+	(ParameterEntry (t,None), IsAssumption Logical)
       in
 	match class_of_constr t with
 	| Some tc ->
@@ -299,7 +299,7 @@ let context ?(hook=fun _ -> ()) l =
 	   match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) false (* inline *) (dummy_loc, id);
+	  [] impl (* implicit *) None (* inline *) (dummy_loc, id);
 	match class_of_constr t with
 	| None -> ()
 	| Some tc -> hook (VarRef id))
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 163f68fd0..b12479b45 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -44,11 +44,11 @@ val interp_assumption :
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   manual_implicits ->
-  bool (** implicit *) -> bool (* inline *) -> variable located -> unit
+  bool (** implicit *) -> inline -> variable located -> unit
 
 val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> manual_implicits ->
-  bool -> bool -> unit
+  bool -> inline -> unit
 
 (** {6 Inductive and coinductive types} *)
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 847278b07..c0ce16cea 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -199,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
           (Local,VarRef id,imps)
       | Global ->
           let k = IsAssumption Conjectural in
-          let kn = declare_constant id (ParameterEntry (t_i,false), k) in
+          let kn = declare_constant id (ParameterEntry (t_i,None), k) in
           (Global,ConstRef kn,imps))
   | Some body ->
       let k = logical_kind_of_goal_kind kind in
@@ -330,7 +330,7 @@ let start_proof_com kind thms hook =
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
   let kn =
-    declare_constant id (ParameterEntry (typ,false),IsAssumption Conjectural) in
+    declare_constant id (ParameterEntry (typ,None),IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
   assumption_message id;
   hook Global (ConstRef kn)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a18340e90..f4fc8714b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -941,6 +941,16 @@ let _ =
       optwrite = (fun b -> Vconv.set_use_vm b) }
 
 let _ =
+  declare_int_option
+    { optsync  = true;
+      optname  = "level of inling duging functor application";
+      optkey   = ["Inline";"Level"];
+      optread  = (fun () -> Some (Flags.get_inline_level ()));
+      optwrite = (fun o ->
+	           let lev = Option.default Flags.default_inline_level o in
+	           Flags.set_inline_level lev) }
+
+let _ =
   declare_bool_option
     { optsync  = true;
       optname  = "use of boxed values";
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 80191b8fd..3091f10c5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -196,6 +196,8 @@ type scheme =
   | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
+type inline = int option (* inlining level, none for no inlining *)
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -226,7 +228,7 @@ type vernac_expr =
         bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
+  | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list