Compatible with MathComp 1.11.0 and coq >= 8.10.
The main addition is the ordered structure iso between [-1, 1] and extended reals ([-oo, +oo]), and the proof of equivalence between the topology induced by the latter iso on extended reals as a pseudo-metric type, and the topology generated by the canonical open basis (i.e. the ]a, b[, ]a, +oo], [-oo, b]).
See the changelog