diff options
| author | Cyril Cohen | 2020-11-04 15:14:14 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-04 15:14:14 +0100 |
| commit | 26a35314966a28880888eefe62ef053f0b9f038f (patch) | |
| tree | d0ae701b54471d80ce78bc8ec645187ec8d285c1 | |
| parent | 6eceb3bc43342c0b4cb03716651a017ce88fed09 (diff) | |
| parent | 8ba40dc7b53e9be38b553e8b13210054c6d2d7b4 (diff) | |
Merge pull request #629 from pi8027/remove-compat-1.9
Remove the mc_1_9 compat module
| -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 := |