diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-04-29 11:13:54 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-04-29 11:13:54 +0200 |
| commit | 016f2dc3aee608b149097cc08d0720227addc18a (patch) | |
| tree | ad36125da2dfc8c0f1ee216beaa3a0c04bf00440 /pretyping/cbv.ml | |
| parent | 5bcccd7ed80acdb9904d5a623f1aba42183803a4 (diff) | |
Fix incorrect cbv reduction of primitive projections. (Bug #4634)
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 43062a0e8..afd86420e 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -310,7 +310,7 @@ and cbv_stack_value info env = function | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) when red_set (info_flags info) fIOTA && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in - cbv_stack_value info env (arg, stk) + cbv_stack_value info env (strip_appl arg stk) (* may be reduced later by application *) | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl) |