diff options
| author | affeldt-aist | 2020-04-15 08:23:35 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-15 08:23:35 +0200 |
| commit | 3bd9af07d734f51de8a7ebde9004c1750400f89b (patch) | |
| tree | 187d7e461a165fde096bd6e531ae6c3d27e659c2 | |
| parent | bdb7ba0daeb2ea8487dfc12578a2d69f44a39751 (diff) | |
| parent | ea6d5dba608a37a8c418638847905202da6d1ab3 (diff) | |
Merge pull request #475 from CohenCyril/ssrnat_deprecated_symbols
adding deprecations 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 aa3983e..9daabce 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -165,8 +165,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). |