last master success https://gitlab.com/coq/coq/-/jobs/1702315162

first master failure https://gitlab.com/coq/coq/-/jobs/1702560186

since the difference is "remove -debug" and fcsl itself was last updated in july I guess mathcomp broke it somehow?

ping @Alexander Gryzlov

hmm, so this is with master version of mathcomp?

it builds fine with 8.14.0 + mathcomp 1.12.0

I'm pretty sure this is linked to https://github.com/math-comp/math-comp/pull/757 because that one touched `eq_in_map`

to my knowledge all projects in Coq's CI that rely on mathcomp are tested with mathcomp `master`

, so likely a MathComp merge is involved

Ok, I found it, they changed the constraint on one of the type params.

builds again with the latest fix (https://github.com/math-comp/math-comp/pull/812)

Alexander Gryzlov has marked this topic as resolved.

Last updated: Feb 06 2023 at 18:03 UTC