From 5a532f2e00d0e3dca8d7079f067c79f2bb1b6b14 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Jun 2019 13:36:39 +0200
Subject: Kernel transparent definition entries have no body universes.

---
 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 7526508c4e..2c434d4edf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff =
   }
   else
   DefinitionEntry {
-    const_entry_body = (p, Univ.ContextSet.empty);
+    const_entry_body = p;
     const_entry_secctx = Some cb.const_hyps;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
-- 
cgit v1.2.3