Specializing the Dyn module to each usecase.

Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.

4 files changed, 16 insertions, 0 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index 85c830ea2..c63875907 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -9,6 +9,8 @@
 open Libnames
 open Pp
 
+module Dyn = Dyn.Make(struct end)
+
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
    wants to work with restricted Coq programs that have only parts of
@@ -158,3 +160,5 @@ let discharge_object ((_,lobj) as node) =
 
 let rebuild_object lobj =
   apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+
+let dump = Dyn.dump
diff --git a/library/libobject.mli b/library/libobject.mli
index 099381897..e49f3fd5c 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -109,3 +109,7 @@ val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
 val relax : bool -> unit
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list
diff --git a/library/summary.ml b/library/summary.ml
index 8e2abbf15..6ef4e131c 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,6 +10,8 @@ open Pp
 open Errors
 open Util
 
+module Dyn = Dyn.Make(struct end)
+
 type marshallable = [ `Yes | `No | `Shallow ]
 type 'a summary_declaration = {
   freeze_function : marshallable -> 'a;
@@ -176,3 +178,5 @@ let ref ?(freeze=fun _ r -> r) ~name x =
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := x) };
   r
+
+let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index 48c9390d0..a35113fd2 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit
 val surgery_summary : frozen -> frozen_bits -> frozen
 val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
 val pointer_equal : frozen_bits -> frozen_bits -> bool
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list