This feature is undocumented and not tested properly, so likely to be buggy. The file interfaces/vectorspace.v seems to be the only one in the whole Coq CI to rely on this feature, since fed14f75b6d114f433ee58d2cfdee61139f6b136, which was supposed to be a cleanup. Given that math-classes keeps compiling after doing it, I believe it is safer to simply remove its use altogether.
This feature is undocumented and not tested properly, so likely to be buggy. The file
interfaces/vectorspace.vseems to be the only one in the whole Coq CI to rely on this feature, since fed14f75b6d114f433ee58d2cfdee61139f6b136, which was supposed to be a cleanup. Given that math-classes keeps compiling after doing it, I believe it is safer to simply remove its use altogether.