Dedicated type for opaque entries in the kernel.

Even more invariants can be enforced this way.

1 files changed, 6 insertions, 6 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ab58321ac7..5dac469a40 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -690,12 +690,12 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    const_entry_secctx = None;
-    const_entry_feedback = None;
-    const_entry_type = Some cb.const_type;
-    const_entry_universes = univs;
-    const_entry_inline_code = cb.const_inline_code }
+    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_secctx = None;
+    opaque_entry_feedback = None;
+    opaque_entry_type = Some cb.const_type;
+    opaque_entry_universes = univs;
+    opaque_entry_inline_code = cb.const_inline_code }
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);