Merge PR #8113: Make universe object Dispose

1 files changed, 10 insertions, 14 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 532339c03c..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
-
-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);
-      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) }
+    { (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