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