From f2b780ab087f8d107820f2fa6f789b83df23d056 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Oct 2020 15:27:44 +0200
Subject: Remove useless libobject for Implicit Type

cache_function is called from add_leaf and after discharging sections,
but default_object is section local.
---
 interp/reserve.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 07160dcf6f..cdc95285fe 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -15,8 +15,6 @@ open Util
 open Pp
 open Names
 open Nameops
-open Libobject
-open Lib
 open Notation_term
 open Notation_ops
 open Globnames
@@ -77,15 +75,11 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NRef (ref,_) -> RefKey(canonical_gr ref), None
   | _ -> Oth, None
 
-let cache_reserved_type (_,(id,t)) =
+let add_reserved_type (id,t) =
   let key = fst (notation_constr_key t) in
   reserve_table := Id.Map.add id t !reserve_table;
   reserve_revtable := keymap_add key (id, t) !reserve_revtable
 
-let in_reserved : Id.t * notation_constr -> obj =
-  declare_object {(default_object "RESERVED-TYPE") with
-    cache_function = cache_reserved_type }
-
 let declare_reserved_type_binding {CAst.loc;v=id} t =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc ~hdr:"declare_reserved_type"
@@ -96,7 +90,7 @@ let declare_reserved_type_binding {CAst.loc;v=id} t =
     user_err ?loc ~hdr:"declare_reserved_type"
     ((Id.print id++str" is already bound to a type"))
   with Not_found -> () end;
-  add_anonymous_leaf (in_reserved (id,t))
+  add_reserved_type (id,t)
 
 let declare_reserved_type idl t =
   List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl)
-- 
cgit v1.2.3