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

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

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f8e8fa9eb9..9c9877fd23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -69,11 +69,9 @@ let subst_reduction_effect (subst,(con,funkey)) =
   (subst_constant subst con,funkey)
 
 let inReductionEffect : Constant.t * string -> obj =
-  declare_object {(default_object "REDUCTION-EFFECT") with
-    cache_function = cache_reduction_effect;
-    open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o);
-    subst_function = subst_reduction_effect;
-    classify_function = (fun o -> Substitute o) }
+  declare_object @@ global_object_nodischarge "REDUCTION-EFFECT"
+    ~cache:cache_reduction_effect
+    ~subst:(Some subst_reduction_effect)
 
 let declare_reduction_effect funkey f =
   if String.Map.mem funkey !effect_table then
-- 
cgit v1.2.3