Christian Doczkal

I still didn't get around to to checking how big the impact on this change would be for `fourcolor`. My fear is that the impact would be significant. Hence, I'm...

I don't think there is anyone currently working on this, but I'd be happy to help you if you want to take up this issue. > Should we start by...

There are a few lemmas that I accumulated over the time. Should I create pull requests (per module) as in #41 or do you want to create an issue per...

@CohenCyril @ybertot Can one of you please check that everyhing that has been added to `ssralg.v` since the `mathcomp-1.12.0` tag and should be exported actually is exported and then update...

@CohenCyril performed the check and said everything is okay for `1.13.0`.

CC: @strub

Just for the record, there is a possibly related issue of the goals buffer not being updated even after successfully reaching the point, if the point is located right after...

@gares would you be willing to self-assign?

If your minimal PR has been merged, I think this issue should be be closed.

This has slumbered for a while, but I factored out the classes/structures and lemmas we use in the graph theory development into a [self-contained library](https://github.com/coq-community/graph-theory/blob/ab5b0d8e2771ed9e7d190a02bf90fff6176bc072/theories/setoid_bigop.v). Comments are welcome.