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.

1 files changed, 29 insertions, 17 deletions

diff --git a/kernel/section.mli b/kernel/section.mli
index 4b23115ca2..c1026a2980 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -13,39 +13,51 @@ open Univ
 
 (** Kernel implementation of sections. *)
 
-type t
-(** Type of sections *)
+type 'a t
+(** Type of sections with additional data ['a] *)
 
-val empty : t
+val empty : 'a t
 
-val is_empty : t -> bool
+val is_empty : 'a t -> bool
 (** Checks whether there is no opened section *)
 
-val is_polymorphic : t -> bool
+val is_polymorphic : 'a t -> bool
 (** Checks whether last opened section is polymorphic *)
 
 (** {6 Manipulating sections} *)
 
-val open_section : poly:bool -> t -> t
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+val open_section : poly:bool -> custom:'a -> 'a t -> '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. *)
+    inside a monomorphic one. A custom data can be attached to this section,
+    that will be returned by {!close_section}. *)
 
-val close_section : t -> t
+val close_section : 'a t -> 'a t * 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. *)
 
 (** {6 Extending sections} *)
 
-val push_local : t -> t
+val push_local : 'a t -> 'a t
 (** Extend the current section with a local definition (cf. push_named). *)
 
-val push_context : Name.t array * UContext.t -> t -> t
+val push_context : Name.t array * UContext.t -> 'a t -> 'a t
 (** Extend the current section with a local universe context. Assumes that the
     last opened section is polymorphic. *)
 
-val push_constant : poly:bool -> Constant.t -> t -> t
+val push_constraints : ContextSet.t -> 'a t -> 'a t
+(** Extend the current section with a global universe context.
+    Assumes that the last opened section is monomorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t
 (** Make the constant as having been defined in this section. *)
 
-val push_inductive : poly:bool -> MutInd.t -> t -> t
+val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 (** Make the inductive block as having been defined in this section. *)
 
 (** {6 Retrieving section data} *)
@@ -64,15 +76,15 @@ type abstr_info = private {
 val empty_segment : abstr_info
 (** Nothing to abstract *)
 
-val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+val segment_of_constant : Environ.env -> Constant.t -> 'a t -> abstr_info
 (** Section segment at the time of the constant declaration *)
 
-val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info
 (** Section segment at the time of the inductive declaration *)
 
-val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
 (** Section segments of all declarations from this section. *)
 
-val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool
 
-val is_polymorphic_univ : Level.t -> t -> bool
+val is_polymorphic_univ : Level.t -> 'a t -> bool