Code simplification in Lib section handling.

Many invariants were implicit in the code, we make them explicit using
dedicated datatypes.

2 files changed, 17 insertions, 15 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 59b55cc16b..cf7f97726a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -433,14 +433,12 @@ type secentry =
 
 type section_data = {
   sec_entry : secentry list;
-  sec_workl : Opaqueproof.work_list;
   sec_abstr : abstr_list;
   sec_poly  : bool;
 }
 
 let empty_section_data ~poly = {
   sec_entry = [];
-  sec_workl = (Names.Cmap.empty,Names.Mindmap.empty);
   sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
   sec_poly  = poly;
 }
@@ -503,7 +501,14 @@ let extract_hyps poly (secs,ohyps) =
   in aux (secs,ohyps)
 
 let instance_from_variable_context =
-  List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+  List.rev_map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let extract_worklist info =
+  let args = instance_from_variable_context info.abstr_ctx in
+  info.abstr_subst, args
+
+let make_worklist (cmap, mmap) =
+  Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
 
 let name_instance inst =
   (* FIXME: this should probably be done at an upper level, by storing the
@@ -522,37 +527,34 @@ let name_instance inst =
   in
   Array.map map (Univ.Instance.to_array inst)
 
-let add_section_replacement f g poly hyps =
+let add_section_replacement g poly hyps =
   match !sectab with
   | [] -> ()
   | s :: sl ->
     let () = check_same_poly poly s in
     let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
-    let inst = Univ.UContext.instance ctx in
-    let nas = name_instance inst in
+    let nas = name_instance (Univ.UContext.instance ctx) in
     let subst, ctx = Univ.abstract_universes nas ctx in
-    let args = instance_from_variable_context (List.rev sechyps) in
     let info = {
       abstr_ctx = sechyps;
       abstr_subst = subst;
       abstr_uctx = ctx;
     } in
     let s = { s with
-      sec_workl = f (inst, args) s.sec_workl;
       sec_abstr = g info s.sec_abstr;
     } in
     sectab := s :: sl
 
 let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f f poly
+    add_section_replacement f poly
 
 let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f f poly
+    add_section_replacement f poly
 
-let replacement_context () = (List.hd !sectab).sec_workl
+let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
 
 let section_segment_of_constant con =
   Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
@@ -585,9 +587,11 @@ let section_instance = let open GlobRef in function
      then Univ.Instance.empty, [||]
      else raise Not_found
   | ConstRef con ->
-      Names.Cmap.find con (fst (List.hd !sectab).sec_workl)
+    let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+    extract_worklist data
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl)
+    let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+    extract_worklist data
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
diff --git a/library/lib.mli b/library/lib.mli
index fe6bf69ec4..b985c8c2bb 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -174,8 +174,6 @@ type abstr_info = private {
   (** Universe quantification, same length as the substitution *)
 }
 
-val instance_from_variable_context : variable_context -> Id.t array
-
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
 val section_segment_of_reference : GlobRef.t -> abstr_info