From e74fce3090323b4d3734f84ee8cf6dc1f5e85953 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 May 2019 00:03:36 +0200
Subject: Abstract away the implementation of side-effects in Safe_typing.

---
 kernel/safe_typing.mli | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..6fcdef9a10 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,11 +43,6 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 type private_constants
 
-val side_effects_of_private_constants :
-  private_constants -> Entries.side_eff list
-(** Return the list of individual side-effects in the order of their
-    creation. *)
-
 val empty_private_constants : private_constants
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
@@ -62,6 +57,9 @@ val inline_private_constants_in_constr :
 val inline_private_constants_in_definition_entry :
   Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
+val push_private_constants : Environ.env -> private_constants -> Environ.env
+(** Push the constants in the environment if not already there. *)
+
 val universes_of_private : private_constants -> Univ.ContextSet.t list
 
 val is_curmod_library : safe_environment -> bool
-- 
cgit v1.2.3


From 3cdaffab75414f3f59386a4b76c6b00c94bc8b0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 May 2019 00:26:56 +0200
Subject: Simplify the private constant API.

We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
---
 kernel/safe_typing.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6fcdef9a10..d6c7022cf5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,8 +48,8 @@ val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_con_of_con : safe_environment -> Constant.t -> private_constants
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
+val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
+(** Constant must be the last definition of the safe_environment. *)
 
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
-- 
cgit v1.2.3