diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-21 18:05:55 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:58:05 -0500 |
| commit | ccdc62a6b4722c38f2b37cbf21b14e5094255390 (patch) | |
| tree | 9dea2af3a7c398cd66a0abd60d6bec6094951ffe /parsing/pcoq.ml4 | |
| parent | f65f8d5a4d9ba437fa2d8af03e2781d841e53007 (diff) | |
Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form
(let x := t in u) a that should be reduced. Maybe a different
decomposition/reduction primitive should be used instead.
Diffstat (limited to 'parsing/pcoq.ml4')
0 files changed, 0 insertions, 0 deletions