diff options
| author | Gaëtan Gilbert | 2019-10-28 15:08:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-28 15:08:31 +0100 |
| commit | 9297352202fa6a43faf266a97a6a07d1df317b9a (patch) | |
| tree | 6f1919e823acc91bffbe53d5c2065a038df86c91 /library/lib.mli | |
| parent | b5d1c31e2d10084935d36a67e0d44b725210b979 (diff) | |
| parent | 252aaae6a6955718609a94b7ae5ac707145d5064 (diff) | |
Merge PR #10952: [library] [nit] Remove unnecessary type alias.
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 17 |
1 files changed, 4 insertions, 13 deletions
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 |