Skip to content

avoid relying on rewrite's implicit revert

Ralf Jung requested to merge ralf/rewrite into master

In https://github.com/coq/coq/pull/13882 it was discovered that rewrite ... in H * behaves really strangely in some cases: it implicitly revert H! This adjusts our code to not rely on that behavior any more (at least in this instance, there might be others).

Merge request reports