From ea6d5dba608a37a8c418638847905202da6d1ab3 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 8 Apr 2020 18:27:09 +0200
Subject: adding depreciations in ssrnat

---
 mathcomp/ssreflect/ssrnat.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index c2f2c52..5051408 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1922,3 +1922,24 @@ End mc_1_10.
 (* Temporary backward compatibility. *)
 Notation odd_add := (deprecate odd_add oddD _) (only parsing).
 Notation odd_sub := (deprecate odd_sub oddB _) (only parsing).
+
+Notation "@ 'homo_inj_lt'" :=
+  (deprecate homo_inj_lt inj_homo_ltn) (at level 10, only parsing) : fun_scope.
+Notation homo_inj_lt := (@homo_inj_lt _) (only parsing).
+Notation "@ 'homo_inj_lt_in'" :=
+  (deprecate homo_inj_lt_in inj_homo_ltn_in) (at level 10, only parsing) : fun_scope.
+Notation homo_inj_lt_in := (@homo_inj_lt_in _ _ _) (only parsing).
+
+Notation "@ 'incr_inj'" :=
+  (deprecate incr_inj incn_inj) (at level 10, only parsing) : fun_scope.
+Notation incr_inj := (@incr_inj _) (only parsing).
+Notation "@ 'incr_inj_in'" :=
+  (deprecate incr_inj_in incn_inj_in) (at level 10, only parsing) : fun_scope.
+Notation incr_inj_in := (@incr_inj_in _ _) (only parsing).
+
+Notation "@ 'decr_inj'" :=
+  (deprecate decr_inj decn_inj) (at level 10, only parsing) : fun_scope.
+Notation decr_inj := (@decr_inj _) (only parsing).
+Notation "@ 'decr_inj_in'" :=
+  (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope.
+Notation decr_inj_in := (@decr_inj_in _ _) (only parsing).
-- 
cgit v1.2.3