Stream: math-comp devs

Topic: backporting ssreflect, ssrbool and ssrfun to Coq

view this post on Zulip Cyril Cohen (Aug 25 2020 at 11:45):

@affeldt-aist to answer your questions, backport should be PRed to Coq as soon as they are merged into math-comp master.

view this post on Zulip Reynald Affeldt (Aug 25 2020 at 12:18):

so maybe I should PR right now?

view this post on Zulip Cyril Cohen (Aug 25 2020 at 12:37):

Yes

view this post on Zulip Reynald Affeldt (Aug 25 2020 at 14:14):

Let's try: https://github.com/coq/coq/pull/12898

Last updated: May 31 2023 at 02:31 UTC