1 files changed, 10 insertions, 0 deletions
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";