Improve and test more proof mode error messages
- Print hypothesis name without [INamed].
- Take some local recursive helper functions out to be bound via
Local Ltac
instead. - Fix some bugs (errors because none of the arms of a match worked) along the way.
Unfortunately I was not sure how to trigger all of these codepaths, so it is possible that I also changed some where the H
already is a string.
@robbertkrebbers If you could provide some testcases that trigger error conditions that are not covered yet, that'd be great.
Fixes #201 (closed)