From 1de15982dceaf28740f49f1d6cba61a5473656b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Dec 2019 18:36:03 +0100
Subject: Export the dynamic type API of libobjects.

---
 library/libobject.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'library/libobject.ml')

diff --git a/library/libobject.ml b/library/libobject.ml
index c9ea6bcff8..54c23ff2d5 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -92,14 +92,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
-- 
cgit v1.2.3


From c2341feb58a233598658eeb68a08395b12715b2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Dec 2019 18:44:06 +0100
Subject: 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.
---
 library/libobject.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'library/libobject.ml')

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
-- 
cgit v1.2.3