diff options
| author | Cyril Cohen | 2018-04-17 19:15:59 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-04-17 19:15:59 +0200 |
| commit | e9e9e87a2140e30425c90debe124f67b42801313 (patch) | |
| tree | 695ffe93bc10c326a3ae66551d735b7bd3333df0 /mathcomp | |
| parent | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff) | |
Removing undocumented compatibility module
I had put this for compatibility with mathcomp 1.6 when we were still using svn, but I am afraid it got under the radar.
We should decide
- if we revert the change of `ltngtP`,
- if we document (and extend) the compatibility module
- or if we just remove the module and keep the change to `ltngtP`
I am personally in favour of the last
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 4533103..cfe0fa3 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1596,15 +1596,3 @@ Ltac nat_congr := first apply: (congr1 (addn X1) _); symmetry end ]. - -Module mc_1_6. - -CoInductive compare_nat m n : bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n true false false - | CompareNatGt of m > n : compare_nat m n false true false - | CompareNatEq of m = n : compare_nat m n false false true. - -Lemma ltngtP m n : compare_nat m n (m < n) (n < m) (m == n). -Proof. by case: ltngtP; constructor. Qed. - -End mc_1_6. |