From 88dfc41e23964cb452092deaa67d2ff975ee2b65 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 5 Oct 2019 12:06:35 +0200
Subject: Section.t is never empty

This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.

We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
---
 kernel/safe_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ae6993b0e2..0b7ca26e09 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,7 +35,7 @@ val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
-val sections_of_safe_env : safe_environment -> section_data Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t option
 
 (** The safe_environment state monad *)
 
-- 
cgit v1.2.3