Andres Erbsen

this makes sense overall. I think it should be possible to have run nondeterministically pick a hart without materializing the oracle sequence, though -- bedrock2 uses a similar semantic style,...

Indeed, seems so -- `- coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]`, confirming [here](https://builds.sr.ht/~andres/job/93786) just in case.

The `coq` target mentioned in my latest comment no longer exists. If there's an alternative already, that's great, let's document it.

It is indeed a shame that this has been neglected so long. Who would be the most appropriate reviewer wrt considerations of using setoid rewriting at scale? I personally feel...

The PR rebeases cleanly but I get an error on push. Might it be that I am missing yet another type of permission, or would the PR author have to...

This is not ready for merge-review, but what is already here is representative of what I am proposing. I would appreciate high-level feedback about scope and strategy. For example, it...

@coq/number-maintainers Could I get a review on this? Thanks!

Thank you for the feedback. Here are quick responses: - :+1: - This is already a fraction of the code from the initial draft, and I worry looking at smaller...

> Some users want to use PArith without having to depend on the whole ZArith and micromega. As already discussed on zulip, the fact that all those dependencies are not...

I did look at it a while ago, I just forgot to list it. IIRC the overall conceptual design is rather similar to how what I am doing here applies...