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


From 3390457252c2cbcc8325858c66baeb0c155d6852 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 20 Jul 2018 14:41:43 +0200
Subject: Don't use an object for polymorphic section universes

---
 interp/declare.ml | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/interp/declare.ml b/interp/declare.ml
index 701f71bf88..2b2ca36edc 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -471,24 +471,20 @@ let assumption_message id =
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
-(** Global universe names, in a different summary *)
+(** Monomorphic universes need to survive sections. *)
 
-type universe_context_decl = polymorphic * Univ.ContextSet.t
-
-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 =
+let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
   declare_object
-    { (default_object "Global universe context state") with
-      cache_function = (fun (na, pi) -> cache_universe_context pi);
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+    { (default_object "Monomorphic section universes") with
+      cache_function = (fun (na, uctx) -> Global.push_context_set false uctx);
+      discharge_function = (fun (_, x) -> Some x);
       classify_function = (fun a -> Dispose) }
 
 let declare_universe_context poly ctx =
-  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
+  if poly then
+    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+  else
+    Lib.add_anonymous_leaf (input_universe_context ctx)
 
 (** Global universes are not substitutive objects but global objects
    bound at the *library* or *module* level. The polymorphic flag is
-- 
cgit v1.2.3