From 0c3c5af90101cfcb0fa228bfefa11376bf40e47e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 19 Jul 2018 21:12:23 +0200
Subject: Universe object is Dispose

---
 interp/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/declare.ml b/interp/declare.ml
index 532339c03c..701f71bf88 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -479,13 +479,13 @@ let cache_universe_context (p, ctx) =
   Global.push_context_set p ctx;
   if p then Lib.add_section_context ctx
 
+(* Universes are Dispose because they are included in the kernel module structure. *)
 let input_universe_context : universe_context_decl -> Libobject.obj =
   declare_object
     { (default_object "Global universe context state") with
       cache_function = (fun (na, pi) -> cache_universe_context pi);
-      load_function = (fun _ (_, pi) -> cache_universe_context pi);
       discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
+      classify_function = (fun a -> Dispose) }
 
 let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
-- 
cgit v1.2.3