diff options
| author | Pierre-Marie Pédrot | 2021-03-22 13:31:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-22 13:31:15 +0100 |
| commit | e4e377f8c73f7e1d845a604eb72ba985bdedc5fd (patch) | |
| tree | 0d501dbb0eb9332a27c6e50289e4932388cc532c | |
| parent | b3347fd5c3164dbe649bd819cdc0ef34b021b47a (diff) | |
| parent | f2b780ab087f8d107820f2fa6f789b83df23d056 (diff) | |
Merge PR #13225: Remove useless libobject for Implicit Type
Reviewed-by: ppedrot
| -rw-r--r-- | interp/reserve.ml | 10 |
1 files 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) |