[library] [nit] Remove unnecessary type alias.

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