diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 69 |
1 files changed, 36 insertions, 33 deletions
diff --git a/library/lib.mli b/library/lib.mli index a8e110c6..26f1718c 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -23,7 +25,6 @@ type node = | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -61,8 +62,6 @@ val pull_to_head : Libnames.object_name -> unit for each of them *) val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name -val add_frozen_state : unit -> unit - (** {6 ... } *) (** The function [contents] gives access to the current entire segment *) @@ -84,8 +83,8 @@ val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path (** Kernel-side names *) -val current_mp : unit -> Names.module_path -val make_kn : Names.Id.t -> Names.kernel_name +val current_mp : unit -> Names.ModPath.t +val make_kn : Names.Id.t -> Names.KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -106,11 +105,11 @@ val find_opening_node : Names.Id.t -> node (** {6 Modules and module types } *) val start_module : - export -> Names.module_ident -> Names.module_path -> + export -> Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.module_path -> + Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Libnames.object_prefix val end_module : @@ -123,11 +122,9 @@ val end_modtype : Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(** [Lib.add_frozen_state] must be called after each of the above functions *) - (** {6 Compilation units } *) -val start_compilation : Names.DirPath.t -> Names.module_path -> unit +val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit val end_compilation_checks : Names.DirPath.t -> Libnames.object_name val end_compilation : Libnames.object_name-> Libnames.object_prefix * library_segment @@ -137,8 +134,8 @@ val end_compilation : val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.module_path -> Names.DirPath.t -val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list +val dp_of_mp : Names.ModPath.t -> Names.DirPath.t +val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list val library_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) @@ -155,37 +152,43 @@ val unfreeze : frozen -> unit val init : unit -> unit -(** XML output hooks *) -val xml_open_section : (Names.Id.t -> unit) Hook.t -val xml_close_section : (Names.Id.t -> unit) Hook.t - (** {6 Section management for discharge } *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * - Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = private { + abstr_ctx : variable_context; + (** Section variables of this prefix *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t -val section_segment_of_constant : Names.constant -> abstr_info -val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info +val section_segment_of_constant : Names.Constant.t -> abstr_info +val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info +val section_segment_of_reference : Globnames.global_reference -> abstr_info + val variable_section_segment_of_reference : Globnames.global_reference -> variable_context - -val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array + +val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit -val add_section_context : Univ.universe_context_set -> unit +val add_section_variable : Names.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 -> - Names.constant -> Context.Named.t -> unit + Names.Constant.t -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.mutual_inductive -> Context.Named.t -> unit + Names.MutInd.t -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive -val discharge_con : Names.constant -> Names.constant +val discharge_kn : Names.MutInd.t -> Names.MutInd.t +val discharge_con : Names.Constant.t -> Names.Constant.t val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t |