iRewrite with a Coq-level equality gives bad error message
In a lambdaRust proof, I tried iRewrite tctx_hasty_val in "Ha''".
. I had forgotten that iRewrite
is for internal equalities only. That shows this error:
Error: No matching clauses for match.
This error is always a bug, at least the tactic should tell me what is wrong. :)
Edited by Ralf Jung