diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:46:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:55:31 +0100 |
| commit | 153d77d00ccbacf22aa5d70ca2c1cacab2749339 (patch) | |
| tree | 98997d190ad1b45f3096473c1015feae55b64efe /library/libobject.mli | |
| parent | 0aba678e885fa53fa649de59eb1d06b4af3a847c (diff) | |
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.
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 4 |
1 files changed, 4 insertions, 0 deletions
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 |