Andrej Dudenhefner

I now fully replaced `CM2` by `MM2` in negative and positive results. Since there is a recent paper [Certified Decision Procedures for Two-Counter Machines](https://drops.dagstuhl.de/opus/volltexte/2022/16297/) which points to the 8.15 branch,...

PR https://github.com/uds-psl/coq-library-undecidability/pull/169 now completely replaces `CM2` by `MM2`.

Since the introduction of `vos` target I started to rely on CI for full compilation in my own branches on `push` instead of local compilation. Not to burn many CPU...

> would you be fine with such a change? I support it. Useful documentation is worth the effort.

I suggest keep it simple. I like to insert `Check` after the mathematically most important theorems, e.g. `Problem_undec : undecidable Problem`. If the overall project is uniformly well-structured (and documented...

> Of course, it is up to them to do so but we can explain how to do it in case the reviewer is not very knowledgeable in Coq. In...

> @DmxLarchey @mrhaandi What do you think? I fully support this.

After a cleanup of `SemiUnification` according to design guidelines discussed with Yannick, I have summarized the main principles in the Wiki: https://github.com/uds-psl/coq-library-undecidability/wiki/Structure-Guidelines Feel free to discuss and extend. Those could...

> Are you fine with that Andrej? Yes, I like the separation of complexity and computability. I also now removed the `L/Complexity` framework to reason about compilation time up to...

After removal of the `ComputableTime` framework (`Computable` suffices) the compilation time went further down to `real 5m11.080s, user 31m13.067s`. Here we start hitting diminishing returns because the critical path is...