@Marie Kerjean indeed, compilation of analysis' master against mathcomp's master seems to fail as @Kazuhiko Sakaguchi suspected because of the new Interval library (real-closed has the same problem)
OK. I will provide a fix.
Sorry, couldn't figure it out right away. :-/
can you tell me where the compilation of the master branch of analysis failed for you ? Was it only renaming issues or was it something else ? I am looking at PR #205 at the same time.
Last updated: Feb 09 2023 at 03:06 UTC