diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-11-25 14:14:54 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-11-25 14:28:06 +0100 |
commit | 32c900252a07ea7d2dd9fe15feb21ef98aee3df7 (patch) | |
tree | f0ded05c6d99135fa960f5a546aedf317ad59e94 /doc | |
parent | 903fe285c008389982d292a494c39ed99aa3e0b5 (diff) |
Typo resulting in bad eta-expansion of destructing let's body.
Revealed by message on coq-club on 24/11/2013.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions