Merge PR #6469: No universe constraints in Let definitions

1 files changed, 7 insertions, 0 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404d..36b75668b2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,13 @@ type 'a definition_entry = {
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
+type section_def_entry = {
+  secdef_body : constr;
+  secdef_secctx : Context.Named.t option;
+  secdef_feedback : Stateid.t option;
+  secdef_type : types option;
+}
+
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry =