Merge PR #8096: Higher-level libobject API for objects with fixed scopes

1 files changed, 4 insertions, 9 deletions

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)))