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.

4 files changed, 0 insertions, 32 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]"]