diff options
| author | Cyril Cohen | 2020-04-08 18:27:09 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-04-10 15:34:31 +0200 |
| commit | ea6d5dba608a37a8c418638847905202da6d1ab3 (patch) | |
| tree | 2281c096b7b00c0a7ed7f56cdb179e65f27039f0 | |
| parent | dc1ea50f04fdaada16f2a27a81ec24859b4ab843 (diff) | |
adding depreciations in ssrnat
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 21 |
2 files changed, 23 insertions, 2 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 96ec16c..de557b4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -162,8 +162,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `lerif_mean_square`, `lerif_AGM2`, `lerif_normC_Re_Creal`, `lerif_Re_Creal`, `lerif_rootC_AGM`. - The following naming inconsistencies have been fixed in `ssrnat.v`: - + `homo_inj_lt(_in)` -> `inj_homo_ltn(in)` - + `(inc|dec)r(_in)` -> `(inc|dev)n(_in)` + + `homo_inj_lt(_in)` -> `inj_homo_ltn(_in)` + + `(inc|dec)r_inj(_in)` -> `(inc|dec)n_inj(_in)` - switching long suffixes to short suffixes + `odd_add` -> `oddD` + `odd_sub` -> `oddB` 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). |