diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /library/lib.mli | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'library/lib.mli')
-rw-r--r-- | library/lib.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5..bb883175 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) @@ -172,7 +173,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na 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_constant : bool (* is_projection *) -> Names.constant -> Context.named_context -> unit val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit |