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

---
 plugins/setoid_ring/newring.ml | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9fea3ddcda..65201d922f 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -394,13 +394,9 @@ let subst_th (subst,th) =
 
 let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
-  declare_object
-    {(default_object "tactic-new-ring-theory") with
-      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = subst_th;
-      classify_function = (fun x -> Substitute x)}
-
+  declare_object @@ global_object_nodischarge "tactic-new-ring-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
 
 let setoid_of_relation env evd a r =
   try
@@ -891,12 +887,9 @@ let subst_th (subst,th) =
 
 let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
-  declare_object
-    {(default_object "tactic-new-field-theory") with
-      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
-      cache_function = cache_th;
-      subst_function = subst_th;
-      classify_function = (fun x -> Substitute x) }
+  declare_object @@ global_object_nodischarge "tactic-new-field-theory"
+    ~cache:cache_th
+    ~subst:(Some subst_th)
 
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
-- 
cgit v1.2.3