Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636).

Reviewed-by: maximedenes
Ack-by: bgregoir
Ack-by: proux01

1 files changed, 5 insertions, 9 deletions

diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 85f7369654..4ad830a298 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -206,15 +206,11 @@ and eval_to_patch env (buff,pl,fv) =
   in
   let tc = patch buff pl slots in
   let vm_env =
-    (* Beware, this may look like a call to [Array.map], but it's not.
-       Calling [Array.map f] when the first argument returned by [f]
-       is a float would lead to [vm_env] being an unboxed Double_array
-       (Tag_val = Double_array_tag) whereas eval_tcode expects a
-       regular array (Tag_val = 0).
-       See test-suite/primitive/float/coq_env_double_array.v
-       for an actual instance. *)
-    let a = Array.make (Array.length fv) crazy_val in
-    Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in
+    (* Environment should look like a closure, so free variables start at slot 2. *)
+    let a = Array.make (Array.length fv + 2) crazy_val in
+    a.(1) <- Obj.magic 2;
+    Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv;
+    a in
   eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =