Context: eq_sorted_irr has been deprecated and renamed to irr_sorted_eq in MathComp 1.12.0 (see math-comp/math-comp#646), and this deprecation alias will be removed in MathComp 1.13.0 (see math-comp/math-comp#727).
This change adds a local alias for irr_sorted_eq (which serves as a compatibility layer for MathComp 1.11.0) in ordtype.v, deprecates and renames eq_sorted_ord to ord_sorted_eq so that it is compatible with the current naming convention of MathComp, and replaces the most occurrences of eq_sorted_irr with ord_sorted_eq.
eq_sorted_irr
has been deprecated and renamed toirr_sorted_eq
in MathComp 1.12.0 (see math-comp/math-comp#646), and this deprecation alias will be removed in MathComp 1.13.0 (see math-comp/math-comp#727).irr_sorted_eq
(which serves as a compatibility layer for MathComp 1.11.0) inordtype.v
, deprecates and renameseq_sorted_ord
toord_sorted_eq
so that it is compatible with the current naming convention of MathComp, and replaces the most occurrences ofeq_sorted_irr
withord_sorted_eq
.