Jason Gross

See also https://github.com/coq/coq/issues/16351

If the feature is restricted to execution (that is, the code must parse in all versions, but it is only executed in some versions), this would allow version-dependent Require, which...

Thank you for diagnosing this. The most straightforward thing to do is to just consider both of these to be valid minimizations. I think if you modify https://github.com/JasonGross/coq-tools/blob/b0ab353f51d4d6ffbee97b2ad6e04fd90846369c/examples/run-example-027.sh#L90-L101 with ```diff...

Oh, I guess I forgot to make the first line optional, try ```diff -Module Export Foo_DOT_A_WRAPPED\. +\(Module Export Foo_DOT_A_WRAPPED\. -Module Export A\. +\)\?Module Export A\. Definition foo : Type\. Admitted\....

Hopefully https://github.com/JasonGross/coq-tools/pull/237 will fix the issue. > I'm not familiar enough with this regex format The format is just that of `grep` (except that both the search pattern and the...

Trying again with https://github.com/JasonGross/coq-tools/pull/239, this time I've tested locally with grep

I don't have merge bits for bedrock2 nor rupicola anymore, and Fiat Crypto can't update until both bedrock2 and rupicola do. CC @andres-erbsen @samuelgruetter

> Thoughts from our users? I like this change. (Should the test-suite get a `Fail Ltac2 ...` example, maybe one of the ones that used to work in the stdlib?)...

Now [on PyPi](https://pypi.org/project/coq-tools/) (the documentation needs some work though). And the CI builds [standalone executables for Mac, Linux, and Windows across a variety of Python versions](https://github.com/JasonGross/coq-tools/actions/runs/6593563085), which I can get...

Releases on GitHub now contain standalone executables