Adapt to https://github.com/math-comp/math-comp/pull/1545#29

proux01 wants to merge 1 commit intomasterrocq-community/gaia:masterfrom

mc1545rocq-community/gaia:mc1545Copy head branch name to clipboard