Merge PR #10952: [library] [nit] Remove unnecessary type alias.

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot

1 files changed, 4 insertions, 10 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