2 files changed, 6 insertions, 2 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 664712dd54..190e14eb1c 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 ee44c8d5f3..b5038996c3 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 *)