TODO: rename `pseudometric`

[affeldt-aist]

analysis/theories/topology_theory/pseudometric_structure.v

Line 77 in 723425a

#[short(type="pseudoMetricType")]

but how? @CohenCyril @mkerjean

[affeldt-aist]

ping @CohenCyril @mkerjean

This is not critical but the sooner the better because this will cause a number of deprecations.

[affeldt-aist]

I still haven't an idea so I postpone.