https://github.com/math-comp/math-comp.github.io/blob/0c5889105ecdf34bae9cb7d994ff4350c711d758/installation.org?plain=1#L36 "At some point, we should recommend rocq-mathcomp, since coq-mathcomp is just a compat metapackage." @proux01
math-comp.github.io/installation.org
Line 36 in 0c58891
"At some point, we should recommend rocq-mathcomp, since coq-mathcomp is just a compat metapackage." @proux01