aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2017-10-31 17:34:31 +0100
committerHugo Herbelin2017-11-02 11:19:08 +0100
commitb0e9d691d6c48fb09b20bb9d98626143eb8b92df (patch)
tree64be23b712cb93804d31cb0190b6aebcfbc90b71
parent767816eece27e6bb8cba0bbf122507bd2a3b77a1 (diff)
Exporting ValTMap for use in Genintern.
-rw-r--r--engine/geninterp.ml2
-rw-r--r--engine/geninterp.mli4
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