diff options
| author | Tej Chajed | 2020-10-15 09:17:15 -0500 |
|---|---|---|
| committer | Tej Chajed | 2020-10-15 09:23:47 -0500 |
| commit | cc06679015013fa26736e10227967cd38be3d6b5 (patch) | |
| tree | e972537c241ce48bd1a28e4679f2516ef8b7dcc4 /kernel | |
| parent | 476520ab32d3e975f6cee8aabcd04ad5fdfbbd77 (diff) | |
Report a useful error for dependent destruction
Similar to `dependent induction`, report an error message for `dependent
destruction` saying that importing `Coq.Program.Equality` is required,
rather than failing at parsing time.
This is a small extension of #605 to cover dependent destruction as
well. Here I also put in some tests.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions