Merge PR #10429: Perform the opaque section variable inference outside of the kernel

Reviewed-by: SkySkimmer
Reviewed-by: gares

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 2d29c3ee19..ca08ba485e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -80,7 +80,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context option;
+  opaque_entry_secctx : Constr.named_context;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;