eg https://gitlab.com/coq/coq/-/jobs/4292681091 which says
- File "./Meta_theory/Models/POF_to_Tarski.v", line 157, characters 0-69: - Error: pattern v2 does not match LHS of dotC - - make: *** [Makefile:810: Meta_theory/Models/POF_to_Tarski.vo] Error 1
we do have geocoq in CI, the same pipeline had https://gitlab.com/coq/coq/-/jobs/4292681194 which succeeded
Maybe it's incompatible with the mathcomp in the bench?
likely, the fix upstream could be as simple as calling "simpl", but I guess it is not in MC's CI, since I don't see an hb branch. CC @Pierre Roux
It's indeed not in MC's CI since it's not in Nix
Here is a fixing PR: https://github.com/GeoCoq/GeoCoq/pull/40
Last updated: Nov 29 2023 at 21:01 UTC