Stream: math-comp analysis

Topic: Two `mathcomp_extra`


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 15:03 UTC