diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/library/lib.mli b/library/lib.mli index 9f9d8c7e5f..f1c9bfca24 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -23,7 +23,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 +60,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 *) @@ -123,8 +120,6 @@ 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 @@ -162,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) 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 = variable_context * Univ.universe_level_subst * Univ.AUContext.t val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t @@ -188,3 +183,5 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant 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 |