@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: Jun 13 2024 at 03:02 UTC