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/safe_typing.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b55293f1c..6e5c9c55ae 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -78,7 +78,8 @@ type 'a effect_entry =
 | PureEntry : unit effect_entry
 
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
-- 
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/safe_typing.mli | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e5c9c55ae..c60e7e893f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,24 +73,27 @@ val is_joined_environment : safe_environment -> bool
 
 (** Insertion of global axioms or definitions *)
 
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
 | ConstantEntry : Entries.constant_entry -> global_declaration
 | OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+
 type exported_private_constant = Constant.t
 
 val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a certificate of its validity *)
+(** returns the main constant *)
 val add_constant :
-  side_effect:'a effect_entry -> Label.t -> global_declaration ->
-    (Constant.t * 'a) safe_transformer
+  Label.t -> global_declaration -> Constant.t safe_transformer
+
+(** Similar to add_constant but also returns a certificate *)
+val add_private_constant :
+  Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer
 
 (** Adding an inductive type *)
 
-- 
cgit v1.2.3


From 221db99a7809cad8f613baa2038fbbd8fb27a691 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 6 Jul 2019 17:30:58 +0200
Subject: Ensure that side-effect declarations reaching the kernel are forced.

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

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c60e7e893f..ec86495db8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ type global_declaration =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 type exported_private_constant = Constant.t
 
-- 
cgit v1.2.3