aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2013-11-25 14:14:54 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2013-11-25 14:28:06 +0100
commit32c900252a07ea7d2dd9fe15feb21ef98aee3df7 (patch)
treef0ded05c6d99135fa960f5a546aedf317ad59e94 /doc
parent903fe285c008389982d292a494c39ed99aa3e0b5 (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