diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 21 |
1 files changed, 21 insertions, 0 deletions
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). |