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

5 files changed, 43 insertions, 89 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 16890ea260..2058837b8e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -621,10 +621,9 @@ let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 let lang () = !lang_ref
 
 let extr_lang : lang -> obj =
-  declare_object
-    {(default_object "Extraction Lang") with
-       cache_function = (fun (_,l) -> lang_ref := l);
-       load_function = (fun _ (_,l) -> lang_ref := l)}
+  declare_object @@ superglobal_object_nodischarge "Extraction Lang"
+    ~cache:(fun (_,l) -> lang_ref := l)
+    ~subst:None
 
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
@@ -648,15 +647,10 @@ let add_inline_entries b l =
 (* Registration of operations for rollback. *)
 
 let inline_extraction : bool * GlobRef.t list -> obj =
-  declare_object
-    {(default_object "Extraction Inline") with
-       cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
-       load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       classify_function = (fun o -> Substitute o);
-       discharge_function = (fun (_,x) -> Some x);
-       subst_function =
-        (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
-    }
+  declare_object @@ superglobal_object "Extraction Inline"
+    ~cache:(fun (_,(b,l)) -> add_inline_entries b l)
+    ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))))
+    ~discharge:(fun (_,x) -> Some x)
 
 (* Grammar entries. *)
 
@@ -685,10 +679,9 @@ let print_extraction_inline () =
 (* Reset part *)
 
 let reset_inline : unit -> obj =
-  declare_object
-    {(default_object "Reset Extraction Inline") with
-       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table)}
+  declare_object @@ superglobal_object_nodischarge "Reset Extraction Inline"
+    ~cache:(fun (_,_)-> inline_table :=  empty_inline_table)
+    ~subst:None
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
@@ -731,13 +724,9 @@ let add_implicits r l =
 (* Registration of operations for rollback. *)
 
 let implicit_extraction : GlobRef.t * int_or_id list -> obj =
-  declare_object
-    {(default_object "Extraction Implicit") with
-       cache_function = (fun (_,(r,l)) -> add_implicits r l);
-       load_function = (fun _ (_,(r,l)) -> add_implicits r l);
-       classify_function = (fun o -> Substitute o);
-       subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
-    }
+  declare_object @@ superglobal_object_nodischarge "Extraction Implicit"
+    ~cache:(fun (_,(r,l)) -> add_implicits r l)
+    ~subst:(Some (fun (s,(r,l)) -> (fst (subst_global s r), l)))
 
 (* Grammar entries. *)
 
@@ -784,12 +773,9 @@ let add_blacklist_entries l =
 (* Registration of operations for rollback. *)
 
 let blacklist_extraction : string list -> obj =
-  declare_object
-    {(default_object "Extraction Blacklist") with
-       cache_function = (fun (_,l) -> add_blacklist_entries l);
-       load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       subst_function = (fun (_,x) -> x)
-    }
+  declare_object @@ superglobal_object_nodischarge "Extraction Blacklist"
+    ~cache:(fun (_,l) -> add_blacklist_entries l)
+    ~subst:None
 
 (* Grammar entries. *)
 
@@ -805,10 +791,9 @@ let print_extraction_blacklist () =
 (* Reset part *)
 
 let reset_blacklist : unit -> obj =
-  declare_object
-    {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
+  declare_object @@ superglobal_object_nodischarge "Reset Extraction Blacklist"
+    ~cache:(fun (_,_)-> blacklist_table := Id.Set.empty)
+    ~subst:None
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
@@ -852,23 +837,14 @@ let find_custom_match pv =
 (* Registration of operations for rollback. *)
 
 let in_customs : GlobRef.t * string list * string -> obj =
-  declare_object
-    {(default_object "ML extractions") with
-       cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
-       load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       classify_function = (fun o -> Substitute o);
-       subst_function =
-        (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
-    }
+  declare_object @@ superglobal_object_nodischarge "ML extractions"
+    ~cache:(fun (_,(r,ids,s)) -> add_custom r ids s)
+    ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)))
 
 let in_custom_matchs : GlobRef.t * string -> obj =
-  declare_object
-    {(default_object "ML extractions custom matchs") with
-       cache_function = (fun (_,(r,s)) -> add_custom_match r s);
-       load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
-       classify_function = (fun o -> Substitute o);
-       subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
-    }
+  declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs"
+    ~cache:(fun (_,(r,s)) -> add_custom_match r s)
+    ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s)))
 
 (* Grammar entries. *)
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 19f954c10d..5d0d17ee6b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -237,7 +237,6 @@ let cache_Function (_,finfos) =
   from_graph := Indmap.add finfos.graph_ind finfos !from_graph
 
 
-let load_Function _  = cache_Function
 let subst_Function (subst,finfos) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst_ind i = Mod_subst.subst_ind subst i
@@ -271,9 +270,6 @@ let subst_Function (subst,finfos) =
       is_general = finfos.is_general
     }
 
-let classify_Function infos = Libobject.Substitute infos
-
-
 let discharge_Function (_,finfos) = Some finfos
 
 let pr_ocst c =
@@ -302,15 +298,11 @@ let pr_table tb =
   Pp.prlist_with_sep fnl pr_info l
 
 let in_Function : function_info -> Libobject.obj =
-  Libobject.declare_object
-    {(Libobject.default_object "FUNCTIONS_DB") with
-       Libobject.cache_function = cache_Function;
-       Libobject.load_function  = load_Function;
-       Libobject.classify_function  = classify_Function;
-       Libobject.subst_function = subst_Function;
-       Libobject.discharge_function = discharge_Function
-(*        Libobject.open_function = open_Function; *)
-    }
+  let open Libobject in
+  declare_object @@ superglobal_object "FUNCTIONS_DB"
+    ~cache:cache_Function
+    ~subst:(Some subst_Function)
+    ~discharge:discharge_Function
 
 
 let find_or_none id =
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 *)
 
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
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)))