Merge PR #11348: Discharge inductive types without rechecking them

Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 8 insertions, 0 deletions

diff --git a/kernel/section.mli b/kernel/section.mli
index fbd3d8254e..37d0dab317 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 
 (** {6 Retrieving section data} *)
 
+val all_poly_univs : 'a t -> Univ.Level.t array
+(** Returns all polymorphic universes, including those from previous
+   sections. Earlier sections are earlier in the array.
+
+    NB: even if the array is empty there may be polymorphic
+   constraints about monomorphic universes, which prevent declaring
+   monomorphic globals. *)
+
 type abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)