diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/geninterp.ml | 2 | ||||
| -rw-r--r-- | engine/geninterp.mli | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml index e79e258fbc..2a1addcd3f 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -47,6 +47,8 @@ struct end +module ValTMap = ValT.Map + module ValReprObj = struct type ('raw, 'glb, 'top) obj = 'top Val.tag diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 492e372adb..ae0b26e594 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -39,6 +39,10 @@ sig val inject : 'a tag -> 'a -> t end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the |