Merge pull request #1878 from proux01/fix-import #677

Job	Run time
rocq-core	1m 1s
coq	52s
mathcomp-analysis-single	14m 26s
mathcomp-classical	2m 52s
mathcomp-reals	1m 55s
mathcomp-experimental-reals	50s
mathcomp-analysis	12m 35s
mathcomp-reals-stdlib	52s
mathcomp-analysis-stdlib	14m 1s
mathcomp-infotheo	7m 4s
	56m 28s

Provide feedback