From 252aaae6a6955718609a94b7ae5ac707145d5064 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 17 Oct 2019 18:03:18 +0200
Subject: [library] [nit] Remove unnecessary type alias.

---
 library/lib.mli | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

(limited to 'library/lib.mli')

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
-- 
cgit v1.2.3