From d929838be77e30db04cd91201542bb52ed3ff7fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 25 Jun 2019 20:57:50 +0200
Subject: Similar purity invariants in the kernel.

---
 kernel/entries.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index bc389e9fcf..47e2f72b0e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,11 +99,14 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-type 'a constant_entry =
-  | DefinitionEntry of definition_entry
-  | OpaqueEntry of 'a const_entry_body opaque_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
+(** Dummy wrapper type discriminable from unit *)
+type 'a seff_wrap = { seff_wrap : 'a }
+
+type _ constant_entry =
+  | DefinitionEntry : definition_entry -> unit constant_entry
+  | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry
+  | ParameterEntry : parameter_entry -> unit constant_entry
+  | PrimitiveEntry : primitive_entry -> unit constant_entry
 
 (** {6 Modules } *)
 
-- 
cgit v1.2.3