From 92006b6cc6b49ed6f892a7e5475f32ca852a9769 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Sep 2019 11:14:48 +0200
Subject: Implement section discharging inside kernel.

This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
---
 kernel/safe_typing.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 10fedc2faf..d3ca642a89 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -27,13 +27,15 @@ val digest_match : actual:vodigest -> required:vodigest -> bool
 
 type safe_environment
 
+type section_data
+
 val empty_environment : safe_environment
 
 val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
-val sections_of_safe_env : safe_environment -> Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t
 
 (** The safe_environment state monad *)
 
@@ -89,9 +91,6 @@ val add_constant :
   side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * 'a) safe_transformer
 
-val add_recipe :
-  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
-
 (** Adding an inductive type *)
 
 val add_mind :
-- 
cgit v1.2.3