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

so maybe I should PR right now?

Yes

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

Last updated: May 31 2023 at 02:31 UTC