Stream: math-comp analysis

Topic: compilation against mathcomp's master


view this post on Zulip Reynald Affeldt (Nov 06 2020 at 08:19):

@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)

view this post on Zulip Kazuhiko Sakaguchi (Nov 06 2020 at 08:28):

OK. I will provide a fix.

view this post on Zulip Reynald Affeldt (Nov 06 2020 at 08:29):

Sorry, couldn't figure it out right away. :-/

view this post on Zulip Marie Kerjean (Nov 09 2020 at 09:08):

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: Aug 11 2022 at 03:02 UTC