diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 30 | ||||
| -rw-r--r-- | library/lib.mli | 2 |
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 |