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

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

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