Guillaume Melquiond

The important piece of information is that the `ocaml-beta` package lives in a separate repository (and so would a `coq-beta` package). So, we still end up with two separate repositories:...

Then, the original post is quite misleading, because the very first sentence is: "to follow what is done with the OCaml compiler in the main Opam repository."

Note that `avoid-version` is only available since Opam 2.1, which is quite recent. That is why even the most recent Opam packages (e.g., rc of OCaml 5) still use `depends:...

As far as I understand, for this proposal to be useful for Coq, the `unboxed` attribute would need to be per constructor. Also, this is not just an optimization in...

> Indeed, you would need some way to do a fine-grained control of which constructor is unboxed. Perhaps this could be done by choosing well the content of the other...

Copied from Zulip: > It is great that you have exponential backoff, but you are missing an important piece. You need to make the sleep length random. For example, if...

> @silene also had a proposal which he mentioned when we talked about naming conventions at a WG last year. It was not so much a proposal than a description...

In Why3, we do not distinguish between module implementations and module interfaces. For instance, your following example works fine once translated to WhyML: ```coq Module M. Axiom a:nat. End M....

> Is that a correct understanding? Yes. As for `M:T`, this is getting added to Why3 and will presumably be part of the next release. The meaning is intermediate between...

Perhaps, it is a bad idea to store the term in the original definition. It might be better for the kernel to just create it on the fly when unfolding...