Has anyone tried to use Equations and mathematical components at the same time? A first issue I encounter is because of eq_refl change of arguments. But it seems the rewrite with multi-rules also does not work.

We use them both in MetaCoq. `rewrite`

and multi-rewrites work, but until Equations 1.2.4 there was a parsing conflict when using `-!`

wait, was that fixed by adding a space (`-!`

-> `- !`

) like `rewrite - !lemma`

? We've wondered about that for months...

(okay we wondered a tiny bit and I refrained from investigating, I was just very flabbergasted)

Yes, the fix before was to add a space. This is no longer needed

I've been annoyed with this for quite some time too ;)

Last updated: Oct 13 2024 at 01:02 UTC