diff options
Diffstat (limited to 'kernel/section.mli')
| -rw-r--r-- | kernel/section.mli | 46 |
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 |