diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/library/lib.mli b/library/lib.mli index 1d77212e9d..9933b762ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names + (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -22,11 +23,9 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list @@ -153,7 +152,7 @@ val unfreeze : frozen -> unit val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = private { abstr_ctx : variable_context; @@ -165,7 +164,7 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Context.Named.t +val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info @@ -179,15 +178,16 @@ val is_in_section : GlobRef.t -> bool val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Context.Named.t -> unit + Constant.t -> Constr.named_context -> unit val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Context.Named.t -> unit + MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) val discharge_kn : MutInd.t -> MutInd.t val discharge_con : Constant.t -> Constant.t +val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_global : GlobRef.t -> GlobRef.t val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : |