diff options
| author | Hugo Herbelin | 2017-03-13 23:06:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-15 14:50:53 +0100 |
| commit | 671e5ad1795b2606a5da9c65758fb0d337c4d14e (patch) | |
| tree | 60de8f2d83355269cb07050d14a97b712bb959d4 /dev | |
| parent | 0e07ace6b6810f70f99fffff924d8c499db18250 (diff) | |
Attempt to improve error message when "apply in" fail.
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions