diff options
| author | Pierre-Marie Pédrot | 2019-12-12 18:44:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-22 14:03:06 +0100 |
| commit | c2341feb58a233598658eeb68a08395b12715b2a (patch) | |
| tree | ba5d4caa869298be94beda0e40767107814954b3 /library | |
| parent | 1de15982dceaf28740f49f1d6cba61a5473656b0 (diff) | |
Remove the hacks relying on hardwired libobject tags.
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
Diffstat (limited to 'library')
| -rw-r--r-- | library/libobject.ml | 2 | ||||
| -rw-r--r-- | library/libobject.mli | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 54c23ff2d5..28d0654444 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -82,8 +82,6 @@ and objects = (Names.Id.t * t) list and substitutive_objects = MBId.t list * algebraic_objects -let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t - module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end) let cache_tab = ref DynMap.empty diff --git a/library/libobject.mli b/library/libobject.mli index c83ad4086a..c25345994a 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -127,8 +127,6 @@ val declare_object_full : val declare_object : 'a object_declaration -> ('a -> obj) -val object_tag : obj -> string - val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit val open_object : int -> object_name * obj -> unit |