Christian Doczkal

> Additionally, there is one interesting implication of the current setup: in the case of guessing, the player is able to influence the game somewhat (by choosing a field and...

@CohenCyril , has there been progress since last year, is there a clear roadmap, or should this be downgraded to a draft and de-milestoned? @ybertot would you be willing to...

> but CI also indicates a similar failure in `graph-theory`, for which I've yet to propose a fix (I'm not set up to compile it right now). If needed, I...

Is there some `nix` command that would allow me to quickly get to the context the CI will be in when trying to build `graph-theory` on top of this PR?

It appears that in the part of `graph-theory` that is checked by the MathComp CI there is only one line that breaks. I noticed that the Nix package used in...

@affeldt-aist Has there been any decision on whether 1.12.0 should maintain compatibility with Coq 8.9 or not? Currently, #599 is milestoned for 1.12.0 and will break compatibility with 8.9. Should...

> not sure I fully understand what exactly needs to be done. @CohenCyril , me neither. So before everything, I think this issue needs some elaboration on what the issue...

> I have a hard time understanding what we want to improve here. I frequently encounter this issue when inductively proving that something is in a transitive relation (i..e, `connect...

Both addresses are from previous affiliations and essentially defunct. The Inria one has has a permanent forward, so maybe use that.

I can confirm this behavior in coq-8.12+mathcomp-1.11.0 > Using `rewrite (@ifN _ (1 < 0)).` also works. > EDIT: using `rewrite (@ifN _ (1 < 0)).` leaves a dangling `bool`....