Cyril Cohen (Oct 20 2022 at 10:30): Cyril Cohen (Oct 20 2022 at 10:30):Hi I'm surprised to see two files named mathcomp_extra.v, one in classical and another one in analysis... @Pierre Roux what is the rationale for not regrouping both in classical?
(Also we should never have two files named in the same way under the mathcomp prefix).
Pierre Roux (Oct 20 2022 at 11:04):@Cyril Cohen I thought both files have different dependencies, but apparently that's not (or no longer) the case. I agree there should not be two files with the same name, I'll open a PR to put everything in classical.
Pierre Roux (Oct 20 2022 at 12:24):@Cyril Cohen there it is, CI green: https://github.com/math-comp/analysis/pull/783
Last updated: Apr 18 2024 at 23:01 UTC