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.ml | |
| 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.ml')
| -rw-r--r-- | library/libobject.ml | 4 |
1 files changed, 4 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 |