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.

1 files changed, 3 insertions, 8 deletions

diff --git a/kernel/section.mli b/kernel/section.mli
index ec863b3b90..fbd3d8254e 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -16,13 +16,8 @@ open Univ
 type 'a t
 (** Type of sections with additional data ['a] *)
 
-val empty : 'a t
-
-val is_empty : 'a t -> bool
-(** Checks whether there is no opened section *)
-
 val depth : 'a t -> int
-(** Number of nested sections (0 if no sections are open) *)
+(** Number of nested sections. *)
 
 (** {6 Manipulating sections} *)
 
@@ -30,13 +25,13 @@ type section_entry =
 | SecDefinition of Constant.t
 | SecInductive of MutInd.t
 
-val open_section : custom:'a -> 'a t -> 'a t
+val open_section : custom:'a -> 'a t option -> 'a t
 (** Open a new section with the provided universe polymorphic status. Sections
     can be nested, with the proviso that polymorphic sections cannot appear
     inside a monomorphic one. A custom data can be attached to this section,
     that will be returned by {!close_section}. *)
 
-val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+val close_section : 'a t -> 'a t option * section_entry list * ContextSet.t * 'a
 (** Close the current section and returns the entries defined inside, the set
     of global monomorphic constraints added in this section, and the custom data
     provided at the opening of the section. *)