From c20eb3a73c4868533bb50555d1979f5b9d821256 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 08:22:28 +0200
Subject: Enforce that opaque entries carry their type.

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5dac469a40..6cb7a22a15 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -693,7 +693,7 @@ let constant_entry_of_side_effect eff =
     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_type = cb.const_type;
     opaque_entry_universes = univs;
     opaque_entry_inline_code = cb.const_inline_code }
   else
-- 
cgit v1.2.3