diff options
| author | Hugo Herbelin | 2014-10-27 08:03:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-27 09:57:11 +0100 |
| commit | 47828f078ac7359e8e2e1891bc6ef48812bb73a5 (patch) | |
| tree | a64c89566525ff42618ff32736c5a3b6e8979705 /doc/stdlib/Library.tex | |
| parent | be5db64b2478a45f0d6bf183b502bc44de709465 (diff) | |
Ensuring compatibility when an hypothesis used for destruct is
dependent in the goal without being fully applied: it cannot be
erased. This used to work in 8.4 when the hypothesis was in an empty
type. I fixed this and (somehow arbitrarily) generalized the
non-erasing to other inductive types instead of failing.
Diffstat (limited to 'doc/stdlib/Library.tex')
0 files changed, 0 insertions, 0 deletions