aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorMaxime Dénès2016-08-22 15:01:25 +0200
committerMaxime Dénès2016-08-22 15:01:25 +0200
commitc38f0ff80f28624b3cbf4df1e317f133caa94d1d (patch)
treeabf323d73101b2d2d6910bc580e5dd9a4f7f80fc /kernel/cbytecodes.mli
parent687d510cb43db5029fb4545c3b12ac20cf99197a (diff)
parent5ede69c8e67e6de34af2850695ae7ee24f8588ea (diff)
Merge remote-tracking branch 'github/pr/261' into v8.6
Was PR#261: Use a better data structure for VM compilation of free vars.
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r--kernel/cbytecodes.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 6fa0841af9..5f1f09d00c 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -139,11 +139,14 @@ type fv = fv_elem array
closed terms. *)
exception NotClosed
+module FvMap : Map.S with type key = fv_elem
+
(*spiwack: both type have been moved from Cbytegen because I needed them
for the retroknowledge *)
type vm_env = {
size : int; (** length of the list [n] *)
- fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
+ fv_rev : fv_elem list; (** [fvn; ... ;fv1] *)
+ fv_fwd : int FvMap.t; (** reverse mapping *)
}