From 8ba40dc7b53e9be38b553e8b13210054c6d2d7b4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 4 Nov 2020 19:34:53 +0900
Subject: Remove the `mc_1_9` compat module

---
 mathcomp/ssreflect/ssrnat.v | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'mathcomp')

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