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/ltac/extratactics.mlg | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ec2adf065a..47f593ff3e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -531,11 +531,9 @@ let cache_transitivity_lemma (_,(left,lem)) =
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
 let inTransitivity : bool * Constr.t -> obj =
-  declare_object {(default_object "TRANSITIVITY-STEPS") with
-    cache_function = cache_transitivity_lemma;
-    open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
-    subst_function = subst_transitivity_lemma;
-    classify_function = (fun o -> Substitute o) }
+  declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS"
+    ~cache:cache_transitivity_lemma
+    ~subst:(Some subst_transitivity_lemma)
 
 (* Main entry points *)
 
-- 
cgit v1.2.3