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

(limited to 'library/global.mli')

diff --git a/library/global.mli b/library/global.mli
index d689771f0a..f8b1f35f4d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -51,7 +51,9 @@ val export_private_constants :
   Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
-  side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
+  Id.t -> Safe_typing.global_declaration -> Constant.t
+val add_private_constant :
+  Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
-- 
cgit v1.2.3