4 files changed, 35 insertions, 7 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7f607a51c..d8c5ab5e7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
   match idl, objs0 with
   | _,[] -> []
   | id::idl,(id',obj)::tail when Id.equal id id' ->
-    assert (object_has_tag obj "MODULE");
+    assert (String.equal (object_tag obj) "MODULE");
     let mp_id = MPdot(mp0, Label.of_id id) in
     let objs = match idl with
       | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
diff --git a/library/libobject.ml b/library/libobject.ml
index c63875907..f0d281a2d 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,6 +8,7 @@
 
 open Libnames
 open Pp
+open Util
 
 module Dyn = Dyn.Make(struct end)
 
@@ -72,15 +73,25 @@ type dynamic_object_declaration = {
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
 
-let object_tag = Dyn.tag
-let object_has_tag = Dyn.has_tag
+let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
 
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
+let make_dyn (type a) (tag : a Dyn.tag) =
+  let infun x = Dyn.Dyn (tag, x) in
+  let outfun : (Dyn.t -> a) = fun dyn ->
+    let Dyn.Dyn (t, x) = dyn in
+    match Dyn.eq t tag with
+    | None -> assert false
+    | Some Refl -> x
+  in
+  (infun, outfun)
+
 let declare_object_full odecl =
   let na = odecl.object_name in
-  let (infun,outfun) = Dyn.create na in
+  let tag = Dyn.create na in
+  let (infun, outfun) = make_dyn tag in
   let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
   and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
   and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
diff --git a/library/libobject.mli b/library/libobject.mli
index e49f3fd5c..12b1a558f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -99,7 +99,6 @@ val declare_object :
   'a object_declaration -> ('a -> obj)
 
 val object_tag : obj -> string
-val object_has_tag : obj -> string -> bool
 
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
diff --git a/library/summary.ml b/library/summary.ml
index 6ef4e131c..a922e155d 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -22,8 +22,19 @@ let summaries = ref Int.Map.empty
 
 let mangle id = id ^ "-SUMMARY"
 
+let make_dyn (type a) (tag : a Dyn.tag) =
+  let infun x = Dyn.Dyn (tag, x) in
+  let outfun : (Dyn.t -> a) = fun dyn ->
+    let Dyn.Dyn (t, x) = dyn in
+    match Dyn.eq t tag with
+    | None -> assert false
+    | Some Refl -> x
+  in
+  (infun, outfun)
+
 let internal_declare_summary hash sumname sdecl =
-  let (infun, outfun) = Dyn.create (mangle sumname) in
+  let tag = Dyn.create (mangle sumname) in
+  let (infun, outfun) = make_dyn tag in
   let dyn_freeze b = infun (sdecl.freeze_function b)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -166,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids =
   List.filter (fun (id, _) -> List.mem id ids) summaries
 
 let pointer_equal l1 l2 =
+  let ptr_equal d1 d2 =
+    let Dyn.Dyn (t1, x1) = d1 in
+    let Dyn.Dyn (t2, x2) = d2 in
+    match Dyn.eq t1 t2 with
+    | None -> false
+    | Some Refl -> x1 == x2
+    in
   CList.for_all2eq
-    (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+    (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
 
 (** All-in-one reference declaration + registration *)