From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 27 Oct 2015 13:55:45 -0400
Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
 structure.

---
 library/lib.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index 9c4d26c5b2..b67b2b873f 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,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
-- 
cgit v1.2.3


From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 28 Oct 2015 10:03:17 +0100
Subject: lib_stack: API to reorder the libstack

For discharging it is important that constants occur in the libstack
in an order that respects the dependencies among them.  This is
impossible to achieve for private constants when they are exported globally
without this (ugly IMO) api.
---
 library/lib.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index b67b2b873f..bb88317591 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 *)
-- 
cgit v1.2.3