diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 14 |
2 files changed, 2 insertions, 14 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4b264e4..81f1d27 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -431,6 +431,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `mxpoly.v`, we deprecate `scalar_mx_comm`, and advise to use `comm_mxC` instead (with maximal implicit arguments `R` and `n`). +- in `ssrnat.v`, we remove the compatibility module `mc_1_9`. + ### Infrastructure ### Misc diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index ce7407d..99189f7 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1970,20 +1970,6 @@ Ltac nat_congr := first symmetry end ]. -Module mc_1_9. - -Variant compare_nat m n : - bool -> bool -> bool -> bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n true false true false false false - | CompareNatGt of m > n : compare_nat m n false true false true false false - | CompareNatEq of m = n : compare_nat m n true true false false true true. - -Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) - (n < m) (n == m) (m == n). -Proof. by case: ltngtP; constructor. Qed. - -End mc_1_9. - Module mc_1_10. Variant leq_xor_gtn m n : bool -> bool -> Set := |