Adapt to https://github.com/math-comp/math-comp/pull/1354#25

proux01 merged 1 commit intomasterrocq-community/gaia:masterfrom

mc1354rocq-community/gaia:mc1354Copy head branch name to clipboard