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.ml | 39 +++++++++++++++++++++++++++------------
 1 file changed, 27 insertions(+), 12 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index f4f52db53b..cdc8889037 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 		  
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
+type secentry =
+  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+		   Decl_kinds.polymorphic * Univ.universe_context_set)
+  | Context of Univ.universe_context_set
+
 let sectab =
-  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
-		Decl_kinds.polymorphic * Univ.universe_context_set) list *
-		        Opaqueproof.work_list * abstr_list) list)
+  Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
@@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
+	sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+
+let add_section_context ctx =
+  match !sectab with
+    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+    | (vars,repl,abs)::sl ->
+	sectab := (Context ctx :: vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+    | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | ((_,_,poly,ctx)::idl,hyps) -> 
+    | (Variable (_,_,poly,ctx)::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, if poly then Univ.ContextSet.union r ctx else r
+    | (Context ctx :: idl, hyps) ->
+       let l, r = aux (idl, hyps) in
+       l, Univ.ContextSet.union r ctx
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
-
   let rec inst_rec = function
     | (id,b,None,_) :: sign -> id :: inst_rec sign
     | _ :: sign -> inst_rec sign
@@ -437,7 +448,8 @@ let add_section_replacement f g hyps =
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl
+    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn =
 
 let section_instance = function
   | VarRef id ->
-      if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
-	(pi1 (List.hd !sectab))
-      then Univ.Instance.empty, [||]
-      else raise Not_found
+     let eq = function
+       | Variable (id',_,_,_) -> Names.id_eq id id'
+       | Context _ -> false
+     in
+     if List.exists eq (pi1 (List.hd !sectab))
+     then Univ.Instance.empty, [||]
+     else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-- 
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.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index cdc8889037..297441e6e2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -198,6 +198,9 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_stk := (sp,node) :: !lib_stk
 
+let pull_to_head oname =
+  lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
-- 
cgit v1.2.3