From 24eccfc6dfec012da081a0891c397f013cc590e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 May 2019 15:58:05 +0200
Subject: Stub code for handling sections in kernel.

For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
---
 kernel/safe_typing.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fa53fa33fa..4eef43b193 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -140,6 +140,12 @@ val set_allow_sprop : bool -> safe_transformer0
 
 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
 
+(** {6 Interactive section functions } *)
+
+val open_section : poly:bool -> safe_transformer0
+
+val close_section : safe_transformer0
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> ModPath.t safe_transformer
-- 
cgit v1.2.3