affeldt-aist

We close this issue since we now use the deprecation mechanism from Coq, please reopen if needed.

NB: fixing this issue depends on this PR to MathComp https://github.com/math-comp/math-comp/pull/1179

It could maybe help to provide a description for this issue.

(@affeldt-aist do you want to try to do this while you're still in the french timezone?) This is a good idea.

Since normal spaces have made their way into master we can maybe close this issues ? https://github.com/math-comp/analysis/blob/master/theories/topology.v#L427

It might be a good timing to approve this PR. @zstone1 ? @CohenCyril ? The changelog and the PR should be up-to-date. To summarize, the construction of the Lebesgue measure...

There should be 3 CI errors that are unrelated.

Wouah, CI green, thanks @proux01

> For what? For the constant care to the infrastructure!

I rebased on top of master. I've cooked up the following definition to build a linear function in the course of the proof but there may be another, better solution:...