diff options
| author | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
| commit | a205bb9f2a93396aad154ec50f6f122cbd46811c (patch) | |
| tree | cd1ad9834fa9e6391193b377cc4533f9eba702c5 /kernel/clambda.ml | |
| parent | 81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff) | |
| parent | 131ac2af3778a741f5f33e212ef4a57f7a91d20a (diff) | |
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 0727eaeac8..8389dd3262 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -6,7 +6,7 @@ open Constr open Declarations open Cbytecodes open Cinstr -open Pre_env +open Environ open Pp let pr_con sp = str(Names.Label.to_string (Constant.label sp)) @@ -700,6 +700,7 @@ let rec lambda_of_constr env c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env 0 rec_bodies in |