diff options
| -rw-r--r-- | library/lib.ml | 14 | ||||
| -rw-r--r-- | library/lib.mli | 17 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 |
3 files changed, 9 insertions, 24 deletions
diff --git a/library/lib.ml b/library/lib.ml index 80b50b26d0..630c860a61 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -408,18 +408,12 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type abstr_info = Section.abstr_info = private { - abstr_ctx : Constr.named_context; - abstr_subst : Univ.Instance.t; - abstr_uctx : Univ.AUContext.t; -} - let instance_from_variable_context = List.rev %> 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 args = instance_from_variable_context info.Section.abstr_ctx in + info.Section.abstr_subst, args let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () @@ -441,7 +435,7 @@ let section_segment_of_reference = let open GlobRef in function | VarRef _ -> empty_segment let variable_section_segment_of_reference gr = - (section_segment_of_reference gr).abstr_ctx + (section_segment_of_reference gr).Section.abstr_ctx let is_in_section ref = Section.is_in_section (Global.env ()) ref (sections ()) @@ -557,7 +551,7 @@ let discharge_proj_repr = let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) -let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = +let discharge_abstract_universe_context { Section.abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in let ainst = make_abstract_instance auctx in let subst = Instance.append subst ainst in diff --git a/library/lib.mli b/library/lib.mli index cef50a5f3b..a313a62c2e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -164,18 +164,9 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type abstr_info = Section.abstr_info = private { - abstr_ctx : Constr.named_context; - (** Section variables of this prefix *) - abstr_subst : Univ.Instance.t; - (** Actual names of the abstracted variables *) - abstr_uctx : Univ.AUContext.t; - (** Universe quantification, same length as the substitution *) -} - -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 +val section_segment_of_constant : Constant.t -> Section.abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> Section.abstr_info +val section_segment_of_reference : GlobRef.t -> Section.abstr_info val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context @@ -190,4 +181,4 @@ val replacement_context : unit -> Opaqueproof.work_list val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_abstract_universe_context : - abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t + Section.abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/vernac/classes.ml b/vernac/classes.ml index 0a8c4e6b0f..702a3e44a9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -210,7 +210,7 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in try let info = abs_context cl in - let ctx = info.Lib.abstr_ctx in + let ctx = info.Section.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in |