From 1f2a3fe97be66fd3201b9c98e5744953d4149b91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:04:25 +0200
Subject: Cleaning up the previous code by ensuring statically invariants on
 opaque proofs.

We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
---
 kernel/entries.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 1e6bc14935..8c4bd16ae3 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -102,11 +102,10 @@ type 'a const_entry_body = 'a proof_output Future.computation
 (** 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
+type constant_entry =
+  | DefinitionEntry : definition_entry -> constant_entry
+  | ParameterEntry : parameter_entry -> constant_entry
+  | PrimitiveEntry : primitive_entry -> constant_entry
 
 (** {6 Modules } *)
 
-- 
cgit v1.2.3


From 60596e870bcb481673fd3108fc1b6478df5a2621 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:37:42 +0200
Subject: Split the function used to declare side-effects from the standard
 one.

This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
---
 kernel/entries.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8c4bd16ae3..046ea86872 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,9 +99,6 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-(** Dummy wrapper type discriminable from unit *)
-type 'a seff_wrap = { seff_wrap : 'a }
-
 type constant_entry =
   | DefinitionEntry : definition_entry -> constant_entry
   | ParameterEntry : parameter_entry -> constant_entry
-- 
cgit v1.2.3