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.

8 files changed, 29 insertions, 34 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 9e4c6e47fc..70cdd3a2db 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Univ
-open Nametab
 
 
 let qualid_of_level l =
@@ -31,20 +30,6 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
 
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
-  match Level.name u with
-  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
-  | None -> ()
-
-let is_polymorphic l =
-  match Level.name l with
-  | Some n ->
-     (try Nametab.UnivIdMap.find n !universe_map
-      with Not_found -> false)
-  | None -> false
-
 (** Local universe names of polymorphic references *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
diff --git a/engine/univNames.mli b/engine/univNames.mli
index d794d7b744..bd4062ade4 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -13,13 +13,6 @@ open Univ
 val pr_with_global_universes : Level.t -> Pp.t
 val qualid_of_level : Level.t -> Libnames.qualid
 
-(** Global universe information outside the kernel, to handle
-    polymorphic universes in sections that have to be discharged. *)
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-
-(** Is [lvl]  a global polymorphic universe? (ie section polymorphic universe) *)
-val is_polymorphic : Level.t -> bool
-
 (** Local universe name <-> level mapping *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
diff --git a/engine/universes.ml b/engine/universes.ml
index c7e5f654a1..5d0157b2db 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -19,10 +19,6 @@ type univ_name_list = UnivNames.univ_name_list
 let pr_with_global_universes = UnivNames.pr_with_global_universes
 let reference_of_level = UnivNames.qualid_of_level
 
-let add_global_universe = UnivNames.add_global_universe
-
-let is_polymorphic = UnivNames.is_polymorphic
-
 let empty_binders = UnivNames.empty_binders
 
 let register_universe_binders = UnivNames.register_universe_binders
diff --git a/engine/universes.mli b/engine/universes.mli
index 7ca33f47a1..0d3bae4c95 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t
 val reference_of_level : Level.t -> Libnames.qualid
 [@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
 
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
-
-val is_polymorphic : Level.t -> bool
-[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
-
 type universe_binders = UnivNames.universe_binders
 [@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 22e6cf9d1c..23c68b5e18 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -491,7 +491,6 @@ let add_universe src (dp, i) =
   Option.iter (fun poly ->
       let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
       Global.push_context_set poly ctx;
-      UnivNames.add_global_universe level poly;
       if poly then Lib.add_section_context ctx)
     optpoly
 
@@ -580,7 +579,7 @@ let do_constraint poly l =
   let open Univ in
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
-    UnivNames.is_polymorphic level, level
+    Lib.is_polymorphic_univ level, level
   in
   let in_section = Lib.sections_are_opened () in
   let () =
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
diff --git a/test-suite/bugs/closed/8478.v b/test-suite/bugs/closed/8478.v
new file mode 100644
index 0000000000..8baaf8686a
--- /dev/null
+++ b/test-suite/bugs/closed/8478.v
@@ -0,0 +1,11 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Strict Universe Declaration.
+
+Monomorphic Universe v.
+
+Section Foo.
+  Let bar := Type@{u}.
+  Fail Monomorphic Constraint bar.u < v.
+
+End Foo. (* was anomaly undeclared universe due to the constraint *)