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: Mar 28 2024 at 20:01 UTC