search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Don't rely on ssreflect setoid rewrite bug (coq/coq#13882) #26

Closed SkySkimmer closed 3 years ago

SkySkimmer commented 3 years ago

Before the mentioned Coq PR, "rewrite foo in H *" with ssreflect rewrite and a setoid equality would leave the goal with H reverted.

Instead we manually revert H and don't use "in".

This should be backwards compatible and so may be merged now.

clayrat commented 3 years ago

Thanks!