Remove the monomorphic universe libobject.

No need to keep track of it this way now that this data is part of the
kernel.

1 files changed, 1 insertions, 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 *)