Merge PR #10406: Desynchronize the type of proof and kernel entries

Reviewed-by: ejgallego
Reviewed-by: gares

1 files changed, 10 insertions, 2 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a980d22e42..a0cc2974d9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff =
     | OpaqueDef b -> b
     | Def b -> Mod_subst.force_constr b
     | _ -> assert false in
+  if Declareops.is_opaque cb then
+  OpaqueEntry {
+    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_secctx = None;
+    opaque_entry_feedback = None;
+    opaque_entry_type = cb.const_type;
+    opaque_entry_universes = univs;
+  }
+  else
   DefinitionEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    const_entry_body = (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_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
 let export_eff eff =