Fix #8478: Undeclared universe anomaly with sections

Instead of looking into the name-oriented structure we look into the
actual section structures.

Note: together with #8475 this lets us remove UnivNames.add_global_universe.

2 files changed, 17 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 8ebe44890c..07026a9c2a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -440,6 +440,21 @@ let add_section_context ctx =
        check_same_poly true vars;
        sectab := (Context ctx :: vars,repl,abs)::sl
 
+exception PolyFound of bool (* make this a let exception once possible *)
+let is_polymorphic_univ u =
+  try
+    let open Univ in
+    List.iter (fun (vars,_,_) ->
+        List.iter (function
+            | Variable (_,_,poly,(univs,_)) ->
+              if LSet.mem u univs then raise (PolyFound poly)
+            | Context (univs,_) ->
+              if LSet.mem u univs then raise (PolyFound true)
+          ) vars
+      ) !sectab;
+    false
+  with PolyFound b -> b
+
 let extract_hyps (secs,ohyps) =
   let rec aux = function
     | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
diff --git a/library/lib.mli b/library/lib.mli
index 9933b762ba..a7d21060e9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,6 +183,8 @@ val add_section_kn : Decl_kinds.polymorphic ->
   MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
+val is_polymorphic_univ : Univ.Level.t -> bool
+
 (** {6 Discharge: decrease the section level if in the current section } *)
 
 val discharge_kn :  MutInd.t -> MutInd.t