From 3c427cd52ad7e41b4a8cbb7e227b8f79730863b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Jan 2021 16:41:19 +0100
Subject: Do not declare a global universe object when the universe set is
 empty.

---
 vernac/declareUniv.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 834ef0d29a..91ab17575d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -74,6 +74,10 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
       subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
+let input_univ_names (src, l) =
+  if CList.is_empty l then ()
+  else Lib.add_anonymous_leaf (input_univ_names (src, l))
+
 let invent_name (named,cnt) u =
   let rec aux i =
     let na = Id.of_string ("u"^(string_of_int i)) in
@@ -120,7 +124,7 @@ let declare_univ_binders gr pl =
         aux, (id,univ) :: univs)
         (LSet.diff levels named) ((pl,0),univs)
     in
-    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+    input_univ_names (QualifiedUniv l, univs)
 
 let do_universe ~poly l =
   let in_section = Global.sections_are_opened () in
@@ -134,7 +138,7 @@ let do_universe ~poly l =
       Univ.LSet.empty l, Univ.Constraint.empty
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
-  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+  let () = input_univ_names (src, l) in
   DeclareUctx.declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
-- 
cgit v1.2.3