Adapt to Rocq#19987

Open Tragicus opened this issue 9 months ago • 1 comments

https://github.com/coq/coq/pull/19987 refolds terms before using them to instantiate evars, which can make failing unifications worse than they were before. This PR avoids a few failing rewrites by putting succeeding ones beforehand.

Mar 24 '25 13:03 Tragicus

My first round of overlays should be ready soon. Is there something to do here (e.g. rerunning the CI if it is fixed)?

May 15 '25 07:05 Tragicus

please merge

Sep 22 '25 14:09 gares