From 264c208a5eb824c880ef4c46e060185470064df5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 19 Jul 2018 11:41:48 +0200
Subject: Higher-level libobject API for objects with fixed scopes

---
 interp/declare.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index a0ebc3775e..6778fa1e7a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -445,11 +445,9 @@ let assumption_message id =
 (** Monomorphic universes need to survive sections. *)
 
 let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
-  declare_object
-    { (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) }
+  declare_object @@ local_object "Monomorphic section universes"
+    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+    ~discharge:(fun (_, x) -> Some x)
 
 let declare_universe_context poly ctx =
   if poly then
-- 
cgit v1.2.3