Merge PR #11278: Clean libobject stuff

Reviewed-by: SkySkimmer
Reviewed-by: maximedenes

3 files changed, 6 insertions, 19 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 6c47d6c6ae..9cce9b92ad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -243,15 +243,6 @@ let add_discharged_leaf id obj =
   cache_object (oname,newobj);
   add_entry oname (Leaf (AtomicObject newobj))
 
-let add_leaves id objs =
-  let oname = make_foname id in
-  let add_obj obj =
-    add_entry oname (Leaf (AtomicObject obj));
-    load_object 1 (oname,obj)
-  in
-  List.iter add_obj objs;
-  oname
-
 let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
   let oname = make_foname id in
diff --git a/library/lib.mli b/library/lib.mli
index a313a62c2e..0d03046dc2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -65,10 +65,6 @@ val add_anonymous_entry : node -> unit
 val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 
-(** this operation adds all objects with the same name and calls [load_object]
-   for each of them *)
-val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name
-
 (** {6 ... } *)
 
 (** The function [contents] gives access to the current entire segment *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index f1dc63dd9e..f7e4a95a22 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -358,7 +358,7 @@ let find_ring_structure env sigma l =
              spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
     | [] -> assert false
 
-let add_entry (sp,_kn) e =
+let add_entry e =
   from_carrier := Cmap.add e.ring_carrier e !from_carrier
 
 let subst_th (subst,th) =
@@ -403,7 +403,7 @@ let subst_th (subst,th) =
 
 
 let theory_to_obj : ring_info -> obj =
-  let cache_th (name,th) = add_entry name th in
+  let cache_th (_, th) = add_entry th in
   declare_object @@ global_object_nodischarge "tactic-new-ring-theory"
     ~cache:cache_th
     ~subst:(Some subst_th)
@@ -599,7 +599,7 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
   let req = EConstr.to_constr sigma req in
   let sth = EConstr.to_constr sigma sth in
   let _ =
-    Lib.add_leaf name
+    Lib.add_anonymous_leaf
       (theory_to_obj
         { ring_name = name;
           ring_carrier = r;
@@ -814,7 +814,7 @@ let find_field_structure env sigma l =
              spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
     | [] -> assert false
 
-let add_field_entry (sp,_kn) e =
+let add_field_entry e =
   field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier
 
 let subst_th (subst,th) =
@@ -855,7 +855,7 @@ let subst_th (subst,th) =
       field_post_tac = posttac' }
 
 let ftheory_to_obj : field_info -> obj =
-  let cache_th (name,th) = add_field_entry name th in
+  let cache_th (_, th) = add_field_entry th in
   declare_object @@ global_object_nodischarge "tactic-new-field-theory"
     ~cache:cache_th
     ~subst:(Some subst_th)
@@ -925,7 +925,7 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
   let r = EConstr.to_constr sigma r in
   let req = EConstr.to_constr sigma req in
   let _ =
-    Lib.add_leaf name
+    Lib.add_anonymous_leaf
       (ftheory_to_obj
         { field_name = name;
           field_carrier = r;