Hi following the tutorials, we had modify Equations so that funelim also rewrite the equation and simplifies the goal. From what I can see my version that seems up to date coq-equations 1.3+8.19 do not seems to integrate it. Will there be in the release for the Coq platform 8.19 ? Would it be possible ?

We are very close to a release of Coq Platform (the quickchick issue currently being discussed is the last remaining road blocker) - I guess it will be end of next week. A smooth version replacement shouldn't be a problem, but you need to state this in the tracker issue for Equations (https://github.com/mattam82/Coq-Equations/issues/585).

(That is reopen the issue and state the version you want).

Last updated: Oct 13 2024 at 01:02 UTC