There are missing instances at the end of the factory PreTopologicalLmod_isConvexTvs, so it only constructs a uniform space, not a ConvexTvs https://github.com/math-comp/analysis/blob/29f8c5747af6aa4d26e61b29af2a8b554e30bcef/theories/normedtype_theory/tvs.v#L524
There are missing instances at the end of the factory PreTopologicalLmod_isConvexTvs, so it only constructs a uniform space, not a ConvexTvs
analysis/theories/normedtype_theory/tvs.v
Line 524 in 29f8c57