From 46b59c60152148c122ee6ac26cddca42ae4f8430 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 29 Jan 2018 10:55:16 +0100 Subject: [native_compute] Fix evaluation of cofixpoints under primitive projections. --- kernel/nativecode.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ffe19510a..613b2f2ec 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1919,15 +1919,17 @@ let compile_constant env sigma prefix ~interactive con cb = let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; asw_reloc = tbl; asw_finite = true } in let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in let _, arity = tbl.(0) in let ci_uid = fresh_lname Anonymous in let cargs = Array.init arity (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) in let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in let gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in -- cgit v1.2.3