Just want to re-boost this! I'm really glad that people are spending time improving the usability of theorem prover tooling. It's something that could really use more care and attention! The tech is incredible, but full of paper cuts. Work like this really helps!
Quote Tweet
Another thing I find useful as a Coq plugin developer is custom error messages. If your user sees the error Coq gives you, she has no context for what your automation was doing! So I wrapped user_err, and now I'm forced to explain errors to my user
github.com/uwplse/fix-to-