From 7e70815c2f326518c71f25fd9b222281a757572b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Sep 2019 00:02:17 +0200
Subject: Remove the monomorphic universe libobject.

No need to keep track of it this way now that this data is part of the
kernel.
---
 tactics/declare.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index bd47fc147e..e418240d3a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -35,11 +35,6 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Monomorphic universes need to survive sections. *)
 
-let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
-  declare_object @@ local_object "Monomorphic section universes"
-    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
-    ~discharge:(fun (_, x) -> Some x)
-
 let name_instance inst =
   let map lvl = match Univ.Level.name lvl with
     | None -> (* Having Prop/Set/Var as section universes makes no sense *)
@@ -65,7 +60,7 @@ let declare_universe_context ~poly ctx =
     let nas = name_instance (Univ.UContext.instance uctx) in
     Global.push_section_context (nas, uctx)
   else
-    Lib.add_anonymous_leaf (input_universe_context ctx)
+    Global.push_context_set false ctx
 
 (** Declaration of constants and parameters *)
 
-- 
cgit v1.2.3