Merge PR #11307: Remove the hacks relying on hardwired libobject tags.

Reviewed-by: maximedenes

1 files changed, 5 insertions, 9 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index c9ea6bcff8..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
@@ -92,14 +90,12 @@ let declare_object_full odecl =
   let na = odecl.object_name in
   let tag = Dyn.create na in
   let () = cache_tab := DynMap.add tag odecl !cache_tab in
-  let infun v = Dyn.Dyn (tag, v) in
-  let outfun v = match Dyn.Easy.prj v tag with
-  | None -> assert false
-  | Some v -> v
-  in
-  (infun,outfun)
+  tag
 
-let declare_object odecl = fst (declare_object_full odecl)
+let declare_object odecl =
+  let tag = declare_object_full odecl in
+  let infun v = Dyn.Dyn (tag, v) in
+  infun
 
 let cache_object (sp, Dyn.Dyn (tag, v)) =
   let decl = DynMap.find tag !cache_tab in