Remove the unused opaque_entry_inline_code field from opaque entries.

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6cb7a22a15..a0cc2974d9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -695,7 +695,7 @@ let constant_entry_of_side_effect eff =
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
-    opaque_entry_inline_code = cb.const_inline_code }
+  }
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);