Guillaume Melquiond

Yes, the whole point of creating this package is so that no relicensing of Coq's code is needed in the first place anyway.

Unfortunately, I am no Dune expert, so I have no clue why this is a bug and what `:standard` means.

If you did not make a typo, it means that the proposed command line contains an awful lot of duplicated options. Thus, even if it is not perfect, I much...

> Should we let Dune automatically add `-O2 -fno-strict-aliasing -fwrapv -fPIC` to the set of flags, or should we handle this by hand? It depends. Flag `-fPIC` is forced upon...

Done, thanks.

I do not intuitively understand what `Deactivate Notation "_ + _" (in custom foo, only printing) : scope` means. Does it mean that the notation is now only used for...

Regarding the size of binaries, we had the same issue with Why3. Users were complaining about having 15 binaries of 20MB each. By being a bit creative during compilation and...

I would hope so. In fact, the `dune` branch of Why3 supports it too, but it seems to requires `dune-site` to work properly. Anyway, the idea is quite simple. Just...

> The main issue for including coqutil (even in the extended level) would be if there is no one committing to make timely releases when new Coq versions are released....

You seem to imply that the `checksum` field was meant for cryptography use in Opam. As far as I know, the field is only there to ensure the integrity of...