Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.
requested to merge herbelin/stdpp:master+adapt-coq-pr12950-notation-registering-reworking into master
Coq PR #12950, among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing le n m
as either m <= n
or m ≤ n
, due to the order of imports between Utf8.v
and Peano.v
in base.v
.
The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.