From f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 12:15:21 +0100
Subject: generate variance data for section universes (not yet used)

preparation for direct discharge
---
 kernel/section.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'kernel/section.mli')

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