@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