diff options
Diffstat (limited to 'kernel/vmsymtable.ml')
| -rw-r--r-- | kernel/vmsymtable.ml | 14 |
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 = |