From e9e9e87a2140e30425c90debe124f67b42801313 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 17 Apr 2018 19:15:59 +0200
Subject: 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
---
 mathcomp/ssreflect/ssrnat.v | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'mathcomp')

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.
-- 
cgit v1.2.3