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/ssr/ssrview.ml | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 3f974ea063..1aa64d7141 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -45,16 +45,11 @@ module AdaptorDb = struct
     let t' = Detyping.subst_glob_constr subst t in
     if t' == t then a else k, t'
 
-  let classify_adaptor x = Libobject.Substitute x
-
   let in_db =
-    Libobject.declare_object {
-       (Libobject.default_object "VIEW_ADAPTOR_DB")
-    with
-       Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o);
-       Libobject.cache_function = cache_adaptor;
-       Libobject.subst_function = subst_adaptor;
-       Libobject.classify_function = classify_adaptor }
+    let open Libobject in
+    declare_object @@ global_object_nodischarge "VIEW_ADAPTOR_DB"
+      ~cache:cache_adaptor
+      ~subst:(Some subst_adaptor)
 
   let declare kind terms =
     List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term)))
-- 
cgit v1.2.3