Subject: [bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

From: Julien Lepiller <[email-masked]>
Date: Mon, 29 Nov 2021 08:39:23 -0500

>
>Hum, the breakage of coq-bignums or coq-equations is recent.  Because
>using 65234d0 from Nov. 2nd, they are substituable; using [email-masked].
>Or do you mean that [email-masked] is broken with [email-masked]?

I meant to say bignums 8.13 is broken with coq 8.14, and bignums 8.14 is broken with coq 8.13.

>
>In all cases, it appears to me clearer to have:
>
> 1. update coq
> 2. update coq-bignums
> 3. update coq-equations
>
>i.e., update the "compiler" and fix then the breakage introduced by
>this "compiler" upgrade, e.g., upgrade other packages.  We are always
>doing like that, no?

I've always updated dependents first whenever possible (without breaking anything), then the compiler, then the rest that needs the new compiler. However, I've always been careful not to introduce breakage with a commit, even if it's inside a series. I think that's the policiy, but I'm not sure if it overrides the one-change per commit policy.

>Cheers,
>simon