Closed CohenCyril closed 3 years ago
To preserve compatibility with https://github.com/math-comp/math-comp/pull/661
Please merge ASAP, thanks.
To preserve compatibility with https://github.com/math-comp/math-comp/pull/661