diff options
| author | Maxime Dénès | 2018-07-26 11:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 11:11:09 +0200 |
| commit | 3f2979c5f0fc289f41cc0e36b9914b3c8f7f77c5 (patch) | |
| tree | bd8f17ee9be6175c879bb1ef972b6fe7f97f13a4 /kernel/cbytegen.ml | |
| parent | b13c954c49f546ecbbc5f73d32e69348408e2ad4 (diff) | |
| parent | 2ff9efcf617318fdfec9966cf3690d1fc4e56da7 (diff) | |
Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 4613cd3214..e336ea922d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -501,6 +501,9 @@ let rec compile_lam env cenv lam sz cont = if Array.is_empty args then compile_fv_elem cenv (FVevar evk) sz cont else + (** Arguments are reversed in evar instances *) + let args = Array.copy args in + let () = Array.rev args in comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont |