| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix incorrect cbv reduction of primitive projections. (Bug #4634) |  Guillaume Melquiond | 2016-04-29 |
| 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. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |