diff options
| author | Kazuhiko Sakaguchi | 2020-12-15 22:05:15 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2021-01-16 00:28:21 +0900 |
| commit | 5f748f7ed9940c0db56e7dadd166f5e69bde6da9 (patch) | |
| tree | d7013ad66741ab20ec57e29ad013daf55f4dd902 | |
| parent | 68fab9412b287079164aab5f3eda71fcd65df8cc (diff) | |
Drop support for Coq 8.10 and deprecate the `deprecate` notation
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.
28 files changed, 418 insertions, 1468 deletions
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 9f45794..f665988 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - coq: [ "8.11", "8.10", "8.12" ] + coq: [ "8.11", "8.12" ] steps: - name: Get branch shortname run: echo "##[set-output name=name;]$(echo ${GITHUB_REF#refs/heads/})" diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4b0d207..8a5c7f0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -89,9 +89,6 @@ make-coq-latest: variables: - $CRON_MODE == "nightly" -coq-8.10: - extends: .opam-build-once - coq-8.11: extends: .opam-build-once @@ -162,11 +159,6 @@ test-coq-8.11: variables: COQ_VERSION: "8.11" -test-coq-8.10: - extends: .test-once - variables: - COQ_VERSION: "8.10" - # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: stage: test @@ -211,11 +203,6 @@ test-coq-8.10: - make -j "${NJOBS}" - make install -ci-fourcolor-8.10: - extends: .ci-fourcolor - variables: - COQ_VERSION: "8.10" - ci-fourcolor-8.11: extends: .ci-fourcolor variables: @@ -246,11 +233,6 @@ ci-fourcolor-dev: - make -j "${NJOBS}" - make install -ci-odd-order-8.10: - extends: .ci-odd-order - variables: - COQ_VERSION: "8.10" - ci-odd-order-8.11: extends: .ci-odd-order variables: @@ -281,11 +263,6 @@ ci-odd-order-dev: - opam pin add -n -k path coq-lemma-overloading . - opam install -y -v -j "${NJOBS}" coq-lemma-overloading -ci-lemma-overloading-8.10: - extends: .ci-lemma-overloading - variables: - COQ_VERSION: "8.10" - ci-lemma-overloading-8.11: extends: .ci-lemma-overloading variables: @@ -316,11 +293,6 @@ ci-lemma-overloading-dev: - opam pin add -n -k path coq-mathcomp-bigenough . - opam install -y -v -j "${NJOBS}" coq-mathcomp-bigenough -ci-bigenough-8.10: - extends: .ci-bigenough - variables: - COQ_VERSION: "8.10" - ci-bigenough-8.11: extends: .ci-bigenough variables: @@ -352,11 +324,6 @@ ci-bigenough-dev: - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed -ci-real-closed-8.10: - extends: .ci-real-closed - variables: - COQ_VERSION: "8.10" - ci-real-closed-8.11: extends: .ci-real-closed variables: @@ -388,11 +355,6 @@ ci-real-closed-dev: - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-finmap - opam install -y -v -j "${NJOBS}" coq-mathcomp-finmap -ci-finmap-8.10: - extends: .ci-finmap - variables: - COQ_VERSION: "8.10" - ci-finmap-8.11: extends: .ci-finmap variables: @@ -424,11 +386,6 @@ ci-finmap-dev: - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-multinomials - opam install -y -v -j "${NJOBS}" coq-mathcomp-multinomials -ci-multinomials-8.10: - extends: .ci-multinomials - variables: - COQ_VERSION: "8.10" - ci-multinomials-8.11: extends: .ci-multinomials variables: @@ -552,9 +509,6 @@ ci-fcsl-pcm-dev: variables: - $CRON_MODE == "nightly" -mathcomp-dev_coq-8.10: - extends: .docker-deploy-once - mathcomp-dev_coq-8.11: extends: .docker-deploy-once diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ad3cae2..fd5e2cb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -27,6 +27,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - In `ssralg.v` and `ssrint.v`, the nullary ring notations `-%R`, `+%R`, `*%R`, `*:%R`, and `*~%R` are now declared in `fun_scope`. +- across the library, the deprecation mechanism to use has been changed from the + `deprecate` notation to the `deprecated` attribute (cf. Removed section). + ### Renamed - in `path.v`, @@ -35,6 +38,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Removed +- in `ssreflect.v`, the `deprecate` notation has been deprecated. Use the + `deprecated` attribute instead (cf. Changed section). + +- in `seq.v`, `iota_add` has been deprecated. Use `iotaD` instead. + +- in `ssrnat.v` and `ssrnum.v`, deprecation aliases and the `mc_1_10` + compatibility modules introduced in MathComp 1.11+beta1 have been removed. + ### Infrastructure ### Misc diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam index b34b7c7..1c84adf 100644 --- a/coq-mathcomp-ssreflect.opam +++ b/coq-mathcomp-ssreflect.opam @@ -9,7 +9,7 @@ license: "CECILL-B" build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] install: [ make "-C" "mathcomp/ssreflect" "install" ] -depends: [ "coq" { ((>= "8.10" & < "8.14~") | (= "dev"))} ] +depends: [ "coq" { ((>= "8.11" & < "8.14~") | (= "dev"))} ] tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ] authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index b1603e6..2548614 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -31,7 +31,7 @@ TGTS?= H:= $(if $(VERBOSE),,@) # not used yet TOP = $(dir $(lastword $(MAKEFILE_LIST))) COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS) -COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq VDFILE=".coqdeps.test-suite" $(COQMAKEOPTIONS) +COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS) BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \ | wc -l | sed 's/ *//g') @@ -153,7 +153,6 @@ doc: __always__ Makefile.coq . ../etc/utils/builddoc_lib.sh; \ cd _build_doc && mangle_sources $(COQFILES) +cd _build_doc && $(COQMAKE) - cd _build_doc && if [ ! -f .Makefile.coq.d ] ; then cp .coqdeps.d .Makefile.coq.d ; fi #can be removed when coq-8.10 compatibility is dropped cd _build_doc && grep -v vio: .Makefile.coq.d > depend cd _build_doc && cat depend | ../../etc/buildlibgraph $(COQFILES) > htmldoc/depend.js cd _build_doc && $(COQBIN)coqdoc -t "Mathematical Components" \ diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 3efe76d..c99ef61 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1075,11 +1075,11 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. Qed. -Notation "@ 'coprimez_expl'" := - (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimez_expr'" := - (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope. -Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing). -Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing). -Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing). -Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMl instead.")] +Notation coprimez_mull := coprimezMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMr instead.")] +Notation coprimez_mulr := coprimezMr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXl instead.")] +Notation coprimez_expl := coprimezXl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXr instead.")] +Notation coprimez_expr := coprimezXr (only parsing). diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 067a457..469c765 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -868,444 +868,197 @@ Proof. exact: itv_splitUeq. Qed. End mc_1_11. -(* Use `Order.lteif` instead of `lteif`. (`deprecate` does not accept a *) -(* qualified name.) *) -Local Notation lteif := Order.lteif (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")] Notation "@ 'lersif'" := - ((fun _ (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b)) - (deprecate lersif lteif)) + (fun (R : numDomainType) x y b => @Order.lteif _ R x y (~~ b)) (at level 10, only parsing). -Notation lersif := (@lersif _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use Order.lteif instead.")] +Notation lersif := (fun x y b => @Order.lteif _ _ x y (~~ b)) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use [_ < _ ?<= if _] instead.")] Notation "x <= y ?< 'if' b" := - ((fun _ => x < y ?<= if ~~ b) (deprecate lersif lteif)) - (at level 70, y at next level, only parsing) : ring_scope. + (x < y ?<= if ~~ b) (at level 70, y at next level, only parsing) : ring_scope. (* LersifPo *) -Notation "@ 'subr_lersifr0'" := - ((fun _ => @mc_1_11.subr_lersifr0) (deprecate subr_lersifr0 subr_lteifr0)) - (at level 10, only parsing). - -Notation subr_lersifr0 := (@subr_lersifr0 _) (only parsing). - -Notation "@ 'subr_lersif0r'" := - ((fun _ => @mc_1_11.subr_lersif0r) (deprecate subr_lersif0r subr_lteif0r)) - (at level 10, only parsing). - -Notation subr_lersif0r := (@subr_lersif0r _) (only parsing). - -Notation subr_lersif0 := - ((fun _ => @mc_1_11.subr_lersif0) (deprecate subr_lersif0 subr_lteif0)) - (only parsing). - -Notation "@ 'lersif_trans'" := - ((fun _ => @mc_1_11.lersif_trans) (deprecate lersif_trans lteif_trans)) - (at level 10, only parsing). - -Notation lersif_trans := (@lersif_trans _ _ _ _ _ _) (only parsing). - -Notation lersif01 := - ((fun _ => @mc_1_11.lersif01) (deprecate lersif01 lteif01)) (only parsing). - -Notation "@ 'lersif_anti'" := - ((fun _ => @mc_1_11.lersif_anti) (deprecate lersif_anti lteif_anti)) - (at level 10, only parsing). - -Notation lersif_anti := (@lersif_anti _) (only parsing). - -Notation "@ 'lersifxx'" := - ((fun _ => @mc_1_11.lersifxx) (deprecate lersifxx lteifxx)) - (at level 10, only parsing). - -Notation lersifxx := (@lersifxx _) (only parsing). - -Notation "@ 'lersifNF'" := - ((fun _ => @mc_1_11.lersifNF) (deprecate lersifNF lteifNF)) - (at level 10, only parsing). - -Notation lersifNF := (@lersifNF _ _ _ _) (only parsing). - -Notation "@ 'lersifS'" := - ((fun _ => @mc_1_11.lersifS) (deprecate lersifS lteifS)) - (at level 10, only parsing). - -Notation lersifS := (@lersifS _ _ _) (only parsing). - -Notation "@ 'lersifT'" := - ((fun _ => @mc_1_11.lersifT) (deprecate lersifT lteifT)) - (at level 10, only parsing). - -Notation lersifT := (@lersifT _) (only parsing). - -Notation "@ 'lersifF'" := - ((fun _ => @mc_1_11.lersifF) (deprecate lersifF lteifF)) - (at level 10, only parsing). - -Notation lersifF := (@lersifF _) (only parsing). - -Notation "@ 'lersif_oppl'" := - ((fun _ => @mc_1_11.lersif_oppl) (deprecate lersif_oppl lteif_oppl)) - (at level 10, only parsing). - -Notation lersif_oppl := (@lersif_oppl _) (only parsing). - -Notation "@ 'lersif_oppr'" := - ((fun _ => @mc_1_11.lersif_oppr) (deprecate lersif_oppr lteif_oppr)) - (at level 10, only parsing). - -Notation lersif_oppr := (@lersif_oppr _) (only parsing). - -Notation "@ 'lersif_0oppr'" := - ((fun _ => @mc_1_11.lersif_0oppr) (deprecate lersif_0oppr lteif_0oppr)) - (at level 10, only parsing). - -Notation lersif_0oppr := (@lersif_0oppr _) (only parsing). - -Notation "@ 'lersif_oppr0'" := - ((fun _ => @mc_1_11.lersif_oppr0) (deprecate lersif_oppr0 lteif_oppr0)) - (at level 10, only parsing). - -Notation lersif_oppr0 := (@lersif_oppr0 _) (only parsing). - -Notation "@ 'lersif_opp2'" := - ((fun _ => @mc_1_11.lersif_opp2) (deprecate lersif_opp2 lteif_opp2)) - (at level 10, only parsing). - -Notation lersif_opp2 := (@lersif_opp2 _) (only parsing). - -Notation lersif_oppE := - ((fun _ => @mc_1_11.lersif_oppE) (deprecate lersif_oppE lteif_oppE)) - (only parsing). - -Notation "@ 'lersif_add2l'" := - ((fun _ => @mc_1_11.lersif_add2l) (deprecate lersif_add2l lteif_add2l)) - (at level 10, only parsing). - -Notation lersif_add2l := (@lersif_add2l _) (only parsing). - -Notation "@ 'lersif_add2r'" := - ((fun _ => @mc_1_11.lersif_add2r) (deprecate lersif_add2r lteif_add2r)) - (at level 10, only parsing). - -Notation lersif_add2r := (@lersif_add2r _) (only parsing). - -Notation lersif_add2 := - ((fun _ => @mc_1_11.lersif_add2) (deprecate lersif_add2 lteif_add2)) - (only parsing). - -Notation "@ 'lersif_subl_addr'" := - ((fun _ => @mc_1_11.lersif_subl_addr) - (deprecate lersif_subl_addr lteif_subl_addr)) - (at level 10, only parsing). - -Notation lersif_subl_addr := (@lersif_subl_addr _) (only parsing). - -Notation "@ 'lersif_subr_addr'" := - ((fun _ => @mc_1_11.lersif_subr_addr) - (deprecate lersif_subr_addr lteif_subr_addr)) - (at level 10, only parsing). - -Notation lersif_subr_addr := (@lersif_subr_addr _) (only parsing). - -Notation lersif_sub_addr := - ((fun _ => @mc_1_11.lersif_sub_addr) - (deprecate lersif_sub_addr lteif_sub_addr)) - (only parsing). - -Notation "@ 'lersif_subl_addl'" := - ((fun _ => @mc_1_11.lersif_subl_addl) - (deprecate lersif_subl_addl lteif_subl_addl)) - (at level 10, only parsing). - -Notation lersif_subl_addl := (@lersif_subl_addl _) (only parsing). - -Notation "@ 'lersif_subr_addl'" := - ((fun _ => @mc_1_11.lersif_subr_addl) - (deprecate lersif_subr_addl lteif_subr_addl)) - (at level 10, only parsing). - -Notation lersif_subr_addl := (@lersif_subr_addl _) (only parsing). - -Notation lersif_sub_addl := - ((fun _ => @mc_1_11.lersif_sub_addl) - (deprecate lersif_sub_addl lteif_sub_addl)) - (only parsing). - -Notation "@ 'lersif_andb'" := - ((fun _ => @mc_1_11.lersif_andb) (deprecate lersif_andb lteif_andb)) - (at level 10, only parsing). - -Notation lersif_andb := (@lersif_andb _) (only parsing). - -Notation "@ 'lersif_orb'" := - ((fun _ => @mc_1_11.lersif_orb) (deprecate lersif_orb lteif_orb)) - (at level 10, only parsing). - -Notation lersif_orb := (@lersif_orb _) (only parsing). - -Notation "@ 'lersif_imply'" := - ((fun _ => @mc_1_11.lersif_imply) (deprecate lersif_imply lteif_imply)) - (at level 10, only parsing). - -Notation lersif_imply := (@lersif_imply _ _ _ _ _) (only parsing). - -Notation "@ 'lersifW'" := - ((fun _ => @mc_1_11.lersifW) (deprecate lersifW lteifW)) - (at level 10, only parsing). - -Notation lersifW := (@lersifW _ _ _ _) (only parsing). - -Notation "@ 'ltrW_lersif'" := - ((fun _ => @mc_1_11.ltrW_lersif) (deprecate ltrW_lersif ltrW_lteif)) - (at level 10, only parsing). - -Notation ltrW_lersif := (@ltrW_lersif _) (only parsing). - -Notation "@ 'lersif_pmul2l'" := - ((fun _ => @mc_1_11.lersif_pmul2l) (deprecate lersif_pmul2l lteif_pmul2l)) - (at level 10, only parsing). - -Notation lersif_pmul2l := (fun b => @lersif_pmul2l _ b _) (only parsing). - -Notation "@ 'lersif_pmul2r'" := - ((fun _ => @mc_1_11.lersif_pmul2r) (deprecate lersif_pmul2r lteif_pmul2r)) - (at level 10, only parsing). - -Notation lersif_pmul2r := (fun b => @lersif_pmul2r _ b _) (only parsing). - -Notation "@ 'lersif_nmul2l'" := - ((fun _ => @mc_1_11.lersif_nmul2l) (deprecate lersif_nmul2l lteif_nmul2l)) - (at level 10, only parsing). - -Notation lersif_nmul2l := (fun b => @lersif_nmul2l _ b _) (only parsing). - -Notation "@ 'lersif_nmul2r'" := - ((fun _ => @mc_1_11.lersif_nmul2r) (deprecate lersif_nmul2r lteif_nmul2r)) - (at level 10, only parsing). - -Notation lersif_nmul2r := (fun b => @lersif_nmul2r _ b _) (only parsing). - -Notation "@ 'real_lersifN'" := - ((fun _ => @mc_1_11.real_lersifN) (deprecate real_lersifN real_lteifNE)) - (at level 10, only parsing). - -Notation real_lersifN := (@real_lersifN _ _ _) (only parsing). - -Notation "@ 'real_lersif_norml'" := - ((fun _ => @mc_1_11.real_lersif_norml) - (deprecate real_lersif_norml real_lteif_norml)) - (at level 10, only parsing). - -Notation real_lersif_norml := - (fun b => @real_lersif_norml _ b _) (only parsing). - -Notation "@ 'real_lersif_normr'" := - ((fun _ => @mc_1_11.real_lersif_normr) - (deprecate real_lersif_normr real_lteif_normr)) - (at level 10, only parsing). - -Notation real_lersif_normr := - (fun b x => @real_lersif_normr _ b x _) (only parsing). - -Notation "@ 'lersif_nnormr'" := - ((fun _ => @mc_1_11.lersif_nnormr) (deprecate lersif_nnormr lteif_nnormr)) - (at level 10, only parsing). - -Notation lersif_nnormr := (fun x => @lersif_nnormr _ _ x _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteifr0 instead.")] +Notation subr_lersifr0 := mc_1_11.subr_lersifr0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0r instead.")] +Notation subr_lersif0r := mc_1_11.subr_lersif0r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subr_lteif0 instead.")] +Notation subr_lersif0 := mc_1_11.subr_lersif0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_trans instead.")] +Notation lersif_trans := mc_1_11.lersif_trans (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif01 instead.")] +Notation lersif01 := mc_1_11.lersif01 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_anti instead.")] +Notation lersif_anti := mc_1_11.lersif_anti (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifxx instead.")] +Notation lersifxx := mc_1_11.lersifxx (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifNF instead.")] +Notation lersifNF := mc_1_11.lersifNF (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifS instead.")] +Notation lersifS := mc_1_11.lersifS (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifT instead.")] +Notation lersifT := mc_1_11.lersifT (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifF instead.")] +Notation lersifF := mc_1_11.lersifF (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppl instead.")] +Notation lersif_oppl := mc_1_11.lersif_oppl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr instead.")] +Notation lersif_oppr := mc_1_11.lersif_oppr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_0oppr instead.")] +Notation lersif_0oppr := mc_1_11.lersif_0oppr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppr0 instead.")] +Notation lersif_oppr0 := mc_1_11.lersif_oppr0 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_opp2 instead.")] +Notation lersif_opp2 := mc_1_11.lersif_opp2 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_oppE instead.")] +Notation lersif_oppE := mc_1_11.lersif_oppE (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2l instead.")] +Notation lersif_add2l := mc_1_11.lersif_add2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2r instead.")] +Notation lersif_add2r := mc_1_11.lersif_add2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_add2 instead.")] +Notation lersif_add2 := mc_1_11.lersif_add2 (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subl_addr instead.")] +Notation lersif_subl_addr := mc_1_11.lersif_subl_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_subr_addr instead.")] +Notation lersif_subr_addr := mc_1_11.lersif_subr_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_sub_addr instead.")] +Notation lersif_sub_addr := mc_1_11.lersif_sub_addr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subl_addl instead.")] +Notation lersif_subl_addl := mc_1_11.lersif_subl_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_subr_addl instead.")] +Notation lersif_subr_addl := mc_1_11.lersif_subr_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lersif_sub_addl instead.")] +Notation lersif_sub_addl := mc_1_11.lersif_sub_addl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_andb instead.")] +Notation lersif_andb := mc_1_11.lersif_andb (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_orb instead.")] +Notation lersif_orb := mc_1_11.lersif_orb (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_imply instead.")] +Notation lersif_imply := mc_1_11.lersif_imply (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifW instead.")] +Notation lersifW := mc_1_11.lersifW (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use ltrW_lteif instead.")] +Notation ltrW_lersif := mc_1_11.ltrW_lersif (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2l instead.")] +Notation lersif_pmul2l := mc_1_11.lersif_pmul2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pmul2r instead.")] +Notation lersif_pmul2r := mc_1_11.lersif_pmul2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2l instead.")] +Notation lersif_nmul2l := mc_1_11.lersif_nmul2l (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nmul2r instead.")] +Notation lersif_nmul2r := mc_1_11.lersif_nmul2r (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteifNE instead.")] +Notation real_lersifN := mc_1_11.real_lersifN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_norml instead.")] +Notation real_lersif_norml := mc_1_11.real_lersif_norml (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use real_lteif_normr instead.")] +Notation real_lersif_normr := mc_1_11.real_lersif_normr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_nnormr instead.")] +Notation lersif_nnormr := mc_1_11.lersif_nnormr (only parsing). (* LersifOrdered *) -Notation "@ 'lersifN'" := - ((fun _ => @mc_1_11.lersifN) (deprecate lersifN lteifNE)) - (at level 10, only parsing). - -Notation lersifN := (@lersifN _) (only parsing). - -Notation "@ 'lersif_norml'" := - ((fun _ => @mc_1_11.lersif_norml) (deprecate lersif_norml lteif_norml)) - (at level 10, only parsing). - -Notation lersif_norml := (@lersif_norml _) (only parsing). - -Notation "@ 'lersif_normr'" := - ((fun _ => @mc_1_11.lersif_normr) (deprecate lersif_normr lteif_normr)) - (at level 10, only parsing). - -Notation lersif_normr := (@lersif_normr _) (only parsing). - -Notation "@ 'lersif_distl'" := - ((fun _ => @mc_1_11.lersif_distl) (deprecate lersif_distl lteif_distl)) - (at level 10, only parsing). - -Notation lersif_distl := (@lersif_distl _) (only parsing). - -Notation "@ 'lersif_minr'" := - ((fun _ => @mc_1_11.lersif_minr) (deprecate lersif_minr lteif_minr)) - (at level 10, only parsing). - -Notation lersif_minr := (@lersif_minr _) (only parsing). - -Notation "@ 'lersif_minl'" := - ((fun _ => @mc_1_11.lersif_minl) (deprecate lersif_minl lteif_minl)) - (at level 10, only parsing). - -Notation lersif_minl := (@lersif_minl _) (only parsing). - -Notation "@ 'lersif_maxr'" := - ((fun _ => @mc_1_11.lersif_maxr) (deprecate lersif_maxr lteif_maxr)) - (at level 10, only parsing). - -Notation lersif_maxr := (@lersif_maxr _) (only parsing). - -Notation "@ 'lersif_maxl'" := - ((fun _ => @mc_1_11.lersif_maxl) (deprecate lersif_maxl lteif_maxl)) - (at level 10, only parsing). - -Notation lersif_maxl := (@lersif_maxl _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteifNE instead.")] +Notation lersifN := mc_1_11.lersifN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_norml instead.")] +Notation lersif_norml := mc_1_11.lersif_norml (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_normr instead.")] +Notation lersif_normr := mc_1_11.lersif_normr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_distl instead.")] +Notation lersif_distl := mc_1_11.lersif_distl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minr instead.")] +Notation lersif_minr := mc_1_11.lersif_minr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_minl instead.")] +Notation lersif_minl := mc_1_11.lersif_minl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxr instead.")] +Notation lersif_maxr := mc_1_11.lersif_maxr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_maxl instead.")] +Notation lersif_maxl := mc_1_11.lersif_maxl (only parsing). (* LersifField *) -Notation "@ 'lersif_pdivl_mulr'" := - ((fun _ => @mc_1_11.lersif_pdivl_mulr) - (deprecate lersif_pdivl_mulr lteif_pdivl_mulr)) - (at level 10, only parsing). - -Notation lersif_pdivl_mulr := - (fun b => @lersif_pdivl_mulr _ b _) (only parsing). - -Notation "@ 'lersif_pdivr_mulr'" := - ((fun _ => @mc_1_11.lersif_pdivr_mulr) - (deprecate lersif_pdivr_mulr lteif_pdivr_mulr)) - (at level 10, only parsing). - -Notation lersif_pdivr_mulr := - (fun b => @lersif_pdivr_mulr _ b _) (only parsing). - -Notation "@ 'lersif_pdivl_mull'" := - ((fun _ => @mc_1_11.lersif_pdivl_mull) - (deprecate lersif_pdivl_mull lteif_pdivl_mull)) - (at level 10, only parsing). - -Notation lersif_pdivl_mull := - (fun b => @lersif_pdivl_mull _ b _) (only parsing). - -Notation "@ 'lersif_pdivr_mull'" := - ((fun _ => @mc_1_11.lersif_pdivr_mull) - (deprecate lersif_pdivr_mull lteif_pdivr_mull)) - (at level 10, only parsing). - -Notation lersif_pdivr_mull := - (fun b => @lersif_pdivr_mull _ b _) (only parsing). - -Notation "@ 'lersif_ndivl_mulr'" := - ((fun _ => @mc_1_11.lersif_ndivl_mulr) - (deprecate lersif_ndivl_mulr lteif_ndivl_mulr)) - (at level 10, only parsing). - -Notation lersif_ndivl_mulr := - (fun b => @lersif_ndivl_mulr _ b _) (only parsing). - -Notation "@ 'lersif_ndivr_mulr'" := - ((fun _ => @mc_1_11.lersif_ndivr_mulr) - (deprecate lersif_ndivr_mulr lteif_ndivr_mulr)) - (at level 10, only parsing). - -Notation lersif_ndivr_mulr := - (fun b => @lersif_ndivr_mulr _ b _) (only parsing). - -Notation "@ 'lersif_ndivl_mull'" := - ((fun _ => @mc_1_11.lersif_ndivl_mull) - (deprecate lersif_ndivl_mull lteif_ndivl_mull)) - (at level 10, only parsing). - -Notation lersif_ndivl_mull := - (fun b => @lersif_ndivl_mull _ b _) (only parsing). - -Notation "@ 'lersif_ndivr_mull'" := - ((fun _ => @mc_1_11.lersif_ndivr_mull) - (deprecate lersif_ndivr_mull lteif_ndivr_mull)) - (at level 10, only parsing). - -Notation lersif_ndivr_mull := - (fun b => @lersif_ndivr_mull _ b _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mulr instead.")] +Notation lersif_pdivl_mulr := mc_1_11.lersif_pdivl_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mulr instead.")] +Notation lersif_pdivr_mulr := mc_1_11.lersif_pdivr_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivl_mull instead.")] +Notation lersif_pdivl_mull := mc_1_11.lersif_pdivl_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_pdivr_mull instead.")] +Notation lersif_pdivr_mull := mc_1_11.lersif_pdivr_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mulr instead.")] +Notation lersif_ndivl_mulr := mc_1_11.lersif_ndivl_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mulr instead.")] +Notation lersif_ndivr_mulr := mc_1_11.lersif_ndivr_mulr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivl_mull instead.")] +Notation lersif_ndivl_mull := mc_1_11.lersif_ndivl_mull (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_ndivr_mull instead.")] +Notation lersif_ndivr_mull := mc_1_11.lersif_ndivr_mull (only parsing). (* IntervalPo *) -Notation "@ 'lersif_in_itv'" := - ((fun _ => @mc_1_11.lersif_in_itv) (deprecate lersif_in_itv lteif_in_itv)) - (at level 10, only parsing). - -Notation lersif_in_itv := (@lersif_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'itv_gte'" := - ((fun _ => @mc_1_11.itv_gte) (deprecate itv_gte itv_ge)) - (at level 10, only parsing). - -Notation itv_gte := (@itv_gte _ _ _ _ _) (only parsing). - -Notation "@ 'ltr_in_itv'" := - ((fun _ => @mc_1_11.ltr_in_itv) (deprecate ltr_in_itv lt_in_itv)) - (at level 10, only parsing). - -Notation ltr_in_itv := (@ltr_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'ler_in_itv'" := - ((fun _ => @mc_1_11.ler_in_itv) (deprecate ler_in_itv lt_in_itv)) - (at level 10, only parsing). - -Notation ler_in_itv := (@ler_in_itv _ _ _ _ _ _) (only parsing). - -Notation "@ 'itv_splitU2'" := - ((fun _ => @mc_1_11.itv_splitU2) (deprecate itv_splitU2 itv_splitUeq)) - (at level 10, only parsing). - -Notation itv_splitU2 := (@itv_splitU2 _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lteif_in_itv instead.")] +Notation lersif_in_itv := mc_1_11.lersif_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use itv_ge instead.")] +Notation itv_gte := mc_1_11.itv_gte (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")] +Notation ltr_in_itv := mc_1_11.ltr_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lt_in_itv instead.")] +Notation ler_in_itv := @mc_1_11.ler_in_itv (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use itv_splitUeq instead.")] +Notation itv_splitU2 := mc_1_11.itv_splitU2 (only parsing). (* `itv_intersection` accepts any `numDomainType` but `Order.meet` accepts *) -(* only `realDomainType`. Use `Order.meet` instead of `itv_meet`. *) +(* only `realDomainType`. *) +#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")] Notation "@ 'itv_intersection'" := - ((fun _ (R : realDomainType) => @Order.meet _ [latticeType of interval R]) - (deprecate itv_intersection itv_meet)) + (fun (R : realDomainType) => @Order.meet _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use Order.meet instead.")] +Notation itv_intersection := + (@Order.meet _ [latticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersection := (@itv_intersection _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")] Notation "@ 'itv_intersection1i'" := - ((fun _ (R : realDomainType) => @meet1x _ [tbLatticeType of interval R]) - (deprecate itv_intersection1i meet1x)) + (fun (R : realDomainType) => @meet1x _ [tbLatticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meet1x instead.")] +Notation itv_intersection1i := + (@meet1x _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersection1i := (@itv_intersection1i _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")] Notation "@ 'itv_intersectioni1'" := - ((fun _ (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R]) - (deprecate itv_intersectioni1 meetx1)) + (fun (R : realDomainType) => @meetx1 _ [tbLatticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meetx1 instead.")] + Notation itv_intersectioni1 := + (@meetx1 _ [tbLatticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersectioni1 := (@itv_intersectioni1 _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")] Notation "@ 'itv_intersectionii'" := - ((fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R]) - (deprecate itv_intersectionii meetxx)) + (fun _ (R : realDomainType) => @meetxx _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. - -Notation itv_intersectionii := (@itv_intersectionii _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use meetxx instead.")] +Notation itv_intersectionii := + (@meetxx _ [latticeType of interval (_ : realDomainType)]) (only parsing). (* IntervalOrdered *) - +#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")] Notation "@ 'itv_intersectionC'" := - ((fun _ (R : realDomainType) => @meetC _ [latticeType of interval R]) - (deprecate itv_intersectionC meetC)) + (fun (R : realDomainType) => @meetC _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. +#[deprecated(since="mathcomp 1.12.0", note="Use meetC instead.")] +Notation itv_intersectionC := + (@meetC _ [latticeType of interval (_ : realDomainType)]) (only parsing). -Notation itv_intersectionC := (@itv_intersectionC _) (only parsing). - +#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")] Notation "@ 'itv_intersectionA'" := - ((fun _ (R : realDomainType) => @meetA _ [latticeType of interval R]) - (deprecate itv_intersectionA meetA)) + (fun (R : realDomainType) => @meetA _ [latticeType of interval R]) (at level 10, only parsing) : fun_scope. - -Notation itv_intersectionA := (@itv_intersectionA _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use meetA instead.")] +Notation itv_intersectionA := + (@meetA _ [latticeType of interval (_ : realDomainType)]) (only parsing). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index e7e0e35..bd39654 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -3146,9 +3146,8 @@ Canonical matrix_finAlgType (R : finComRingType) n' := Hint Resolve comm_mx_scalar comm_scalar_mx : core. -Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar) - (at level 10, only parsing) : fun_scope. -Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use comm_mx_scalar instead.")] +Notation scalar_mx_comm := comm_mx_scalar (only parsing). (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) @@ -3685,6 +3684,5 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) End mxRingOver. End mxOver. -Notation "@ 'map_mx_sub'" := - (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope. -Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use map_mxB instead.")] +Notation map_mx_sub := map_mxB (only parsing). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index d707905..c23cfb1 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -3068,9 +3068,7 @@ Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. -Notation "@ 'mulsmx_addl'" := - (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope. -Notation "@ 'mulsmx_addr'" := - (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope. -Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing). -Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDl instead.")] +Notation mulsmx_addl := mulsmxDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulsmxDr instead.")] +Notation mulsmx_addr := mulsmxDr (only parsing). diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 21e8ada..e74c917 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -2769,27 +2769,19 @@ Qed. End ClosedField. -Notation "@ 'polyC_add'" := - (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_opp'" := - (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_sub'" := - (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_muln'" := - (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_mul'" := - (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope. -Notation "@ 'polyC_inv'" := - (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope. -Notation "@ 'lead_coef_opp'" := - (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope. -Notation "@ 'derivn_sub'" := - (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope. -Notation polyC_add := (@polyC_add _) (only parsing). -Notation polyC_opp := (@polyC_opp _) (only parsing). -Notation polyC_sub := (@polyC_sub _) (only parsing). -Notation polyC_muln := (@polyC_muln _) (only parsing). -Notation polyC_mul := (@polyC_mul _) (only parsing). -Notation polyC_inv := (@polyC_inv _) (only parsing). -Notation lead_coef_opp := (@lead_coef_opp _) (only parsing). -Notation derivn_sub := (@derivn_sub _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCD instead.")] +Notation polyC_add := polyCD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCN instead.")] +Notation polyC_opp := polyCN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCB instead.")] +Notation polyC_sub := polyCB (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCMn instead.")] +Notation polyC_muln := polyCMn (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCM instead.")] +Notation polyC_mul := polyCM (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCV instead.")] +Notation polyC_inv := polyCV (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lead_coefN instead.")] +Notation lead_coef_opp := lead_coefN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use derivnB instead.")] +Notation derivn_sub := derivnB (only parsing). diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 41147fb..05a9ee3 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -624,17 +624,12 @@ Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed. End MonicDivisor. -Notation "@ 'rdivp_addl'" := - (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope. -Notation "@ 'rdivp_addr'" := - (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope. -Notation "@ 'rmodp_add'" := - (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope. -Notation rdivp_addl := - (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing). -Notation rdivp_addr := - (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing). -Notation rmodp_add := (@rmodp_add _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDl instead.")] +Notation rdivp_addl := rdivpDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rdivpDr instead.")] +Notation rdivp_addr := rdivpDr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use rmodpD instead.")] +Notation rmodp_add := rmodpD (only parsing). End RingMonic. @@ -2358,27 +2353,20 @@ End IDomainPseudoDivision. Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core. Hint Resolve dvdp0 : core. -Notation "@ 'dvdp_scalel'" := - (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'dvdp_scaler'" := - (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'dvdp_opp'" := - (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_scalel'" := - (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_scaler'" := - (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_mull'" := - (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprimep_mulr'" := - (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope. -Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing). -Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing). -Notation dvdp_opp := (@dvdp_opp _) (only parsing). -Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing). -Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing). -Notation coprimep_mull := (@coprimep_mull _) (only parsing). -Notation coprimep_mulr := (@coprimep_mulr _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZl instead.")] +Notation dvdp_scalel := dvdpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpZr instead.")] +Notation dvdp_scaler := dvdpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use dvdpNr instead.")] +Notation dvdp_opp := dvdpNr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZl instead.")] +Notation coprimep_scalel := coprimepZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepZr instead.")] +Notation coprimep_scaler := coprimepZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMl instead.")] +Notation coprimep_mull := coprimepMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimepMr instead.")] +Notation coprimep_mulr := coprimepMr (only parsing). End CommonIdomain. @@ -2704,30 +2692,22 @@ Qed. End MoreUnitDivisor. -Notation "@ 'modp_scalel'" := - (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_scaler'" := - (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_opp'" := - (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_add'" := - (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scalel'" := - (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scaler'" := - (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_opp'" := - (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_add'" := - (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope. -Notation modp_scalel := (@modp_scalel _ _) (only parsing). -Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing). -Notation modp_opp := (@modp_opp _ _) (only parsing). -Notation modp_add := (@modp_add _ _) (only parsing). -Notation divp_scalel := (@divp_scalel _ _) (only parsing). -Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing). -Notation divp_opp := (@divp_opp _ _) (only parsing). -Notation divp_add := (@divp_add _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")] +Notation modp_scalel := modpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")] +Notation modp_scaler := modpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")] +Notation modp_opp := modpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")] +Notation modp_add := modpD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")] +Notation divp_scalel := divpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")] +Notation divp_scaler := divpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")] +Notation divp_opp := divpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")] +Notation divp_add := divpD (only parsing). End IdomainUnit. @@ -3192,30 +3172,22 @@ End FieldMap. End FieldDivision. -Notation "@ 'modp_scalel'" := - (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_scaler'" := - (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_opp'" := - (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'modp_add'" := - (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scalel'" := - (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_scaler'" := - (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_opp'" := - (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. -Notation "@ 'divp_add'" := - (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope. -Notation modp_scalel := (@modp_scalel _) (only parsing). -Notation modp_scaler := (@modp_scaler _ _) (only parsing). -Notation modp_opp := (@modp_opp _) (only parsing). -Notation modp_add := (@modp_add _) (only parsing). -Notation divp_scalel := (@divp_scalel _) (only parsing). -Notation divp_scaler := (@divp_scaler _ _) (only parsing). -Notation divp_opp := (@divp_opp _) (only parsing). -Notation divp_add := (@divp_add _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZl instead.")] +Notation modp_scalel := modpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpZr instead.")] +Notation modp_scaler := modpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpN instead.")] +Notation modp_opp := modpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use modpD instead.")] +Notation modp_add := modpD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZl instead.")] +Notation divp_scalel := divpZl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpZr instead.")] +Notation divp_scaler := divpZr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpN instead.")] +Notation divp_opp := divpN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use divpD instead.")] +Notation divp_add := divpD (only parsing). End Field. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index de8b513..a27177d 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -6044,8 +6044,8 @@ Definition imaginary_exists := imaginary_exists. Notation null_fun V := (null_fun V) (only parsing). Notation in_alg A := (in_alg_loc A). -Notation prodrMn := - (fun n A F => deprecate prodrMn prodrMn_const _ n _ A F) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use prodrMn_const instead.")] +Notation prodrMn := prodrMn_const (only parsing). End Theory. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index a51ec47..becacc2 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1778,6 +1778,5 @@ Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. End rpred. -Notation "@ 'polyC_mulrz'" := - (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope. -Notation polyC_mulrz := (@polyC_mulrz _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")] +Notation polyC_mulrz := polyCMz (only parsing). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index dce3ffd..cc04183 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -5395,625 +5395,3 @@ Export Num.NumMixin.Exports Num.RealMixin.Exports. Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports. Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin. - -(* compatibility module *) -Module mc_1_10. -Module Num. -(* If you failed to process the next line in the PG or the CoqIDE, replace *) -(* all the "ssrnum.Num" with "Top.Num" in this module to process them, and *) -(* revert them in order to compile and commit. This problem will be solved *) -(* in Coq 8.10. See also: https://github.com/math-comp/math-comp/pull/270. *) -Export ssrnum.Num. - -Module Import Def. -Export ssrnum.Num.Def. -Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y. -Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x. -End Def. - -Notation min := minr. -Notation max := maxr. - -Module Import Syntax. -Notation "`| x |" := - (@norm _ (@Num.NormedZmodule.numDomain_normedZmodType _) x) : ring_scope. -End Syntax. - -Module Import Theory. -Export ssrnum.Num.Theory. - -Section NumIntegralDomainTheory. -Variable R : numDomainType. -Implicit Types x y z : R. -Definition ltr_def x y : (x < y) = (y != x) && (x <= y) := lt_def x y. -Definition gerE x y : ge x y = (y <= x) := geE x y. -Definition gtrE x y : gt x y = (y < x) := gtE x y. -Definition lerr x : x <= x := lexx x. -Definition ltrr x : x < x = false := ltxx x. -Definition ltrW x y : x < y -> x <= y := @ltW _ _ x y. -Definition ltr_neqAle x y : (x < y) = (x != y) && (x <= y) := lt_neqAle x y. -Definition ler_eqVlt x y : (x <= y) = (x == y) || (x < y) := le_eqVlt x y. -Definition gtr_eqF x y : y < x -> x == y = false := @gt_eqF _ _ x y. -Definition ltr_eqF x y : x < y -> x == y = false := @lt_eqF _ _ x y. -Definition ler_asym : antisymmetric (@ler R) := le_anti. -Definition eqr_le x y : (x == y) = (x <= y <= x) := eq_le x y. -Definition ltr_trans : transitive (@ltr R) := lt_trans. -Definition ler_lt_trans y x z : x <= y -> y < z -> x < z := - @le_lt_trans _ _ y x z. -Definition ltr_le_trans y x z : x < y -> y <= z -> x < z := - @lt_le_trans _ _ y x z. -Definition ler_trans : transitive (@ler R) := le_trans. -Definition lterr := (lerr, ltrr). -Definition lerifP x y C : - reflect (x <= y ?= iff C) (if C then x == y else x < y) := leifP. -Definition ltr_asym x y : x < y < x = false := lt_asym x y. -Definition ler_anti : antisymmetric (@ler R) := le_anti. -Definition ltr_le_asym x y : x < y <= x = false := lt_le_asym x y. -Definition ler_lt_asym x y : x <= y < x = false := le_lt_asym x y. -Definition lter_anti := (=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym). -Definition ltr_geF x y : x < y -> y <= x = false := @lt_geF _ _ x y. -Definition ler_gtF x y : x <= y -> y < x = false := @le_gtF _ _ x y. -Definition ltr_gtF x y : x < y -> y < x = false := @lt_gtF _ _ x y. -Definition normr0 : `|0| = 0 :> R := normr0 _. -Definition normrMn x n : `|x *+ n| = `|x| *+ n := normrMn x n. -Definition normr0P {x} : reflect (`|x| = 0) (x == 0) := normr0P. -Definition normr_eq0 x : (`|x| == 0) = (x == 0) := normr_eq0 x. -Definition normrN x : `|- x| = `|x| := normrN x. -Definition distrC x y : `|x - y| = `|y - x| := distrC x y. -Definition normr_id x : `| `|x| | = `|x| := normr_id x. -Definition normr_ge0 x : 0 <= `|x| := normr_ge0 x. -Definition normr_le0 x : (`|x| <= 0) = (x == 0) := normr_le0 x. -Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x. -Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x. -Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0, - normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN). -End NumIntegralDomainTheory. - -Section NumIntegralDomainMonotonyTheory. -Variables R R' : numDomainType. -Section AcrossTypes. -Variables (D D' : pred R) (f : R -> R'). -Definition ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y} := - ltW_homo (f := f). -Definition ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y} := - ltW_nhomo (f := f). -Definition inj_homo_ltr : - injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltr : - injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y} := - inj_nhomo_lt (f := f). -Definition incr_inj : {mono f : x y / x <= y} -> injective f := - inc_inj (f := f). -Definition decr_inj : {mono f : x y /~ x <= y} -> injective f := - dec_inj (f := f). -Definition lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y} := - leW_mono (f := f). -Definition lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y} := - leW_nmono (f := f). -Definition ltrW_homo_in : - {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}} := - ltW_homo_in (f := f). -Definition ltrW_nhomo_in : - {in D & D', {homo f : x y /~ x < y}} -> - {in D & D', {homo f : x y /~ x <= y}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} -> - {in D & D', {homo f : x y / x < y}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} -> - {in D & D', {homo f : x y /~ x < y}} := - inj_nhomo_lt_in (f := f). -Definition incr_inj_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decr_inj_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lerW_mono_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}} := - leW_mono_in (f := f). -Definition lerW_nmono_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}} := - leW_nmono_in (f := f). -End AcrossTypes. -Section NatToR. -Variables (D D' : pred nat) (f : nat -> R). -Definition ltnrW_homo : - {homo f : m n / (m < n)%N >-> m < n} -> - {homo f : m n / (m <= n)%N >-> m <= n} := - ltW_homo (f := f). -Definition ltnrW_nhomo : - {homo f : m n / (n < m)%N >-> m < n} -> - {homo f : m n / (n <= m)%N >-> m <= n} := - ltW_nhomo (f := f). -Definition inj_homo_ltnr : injective f -> - {homo f : m n / (m <= n)%N >-> m <= n} -> - {homo f : m n / (m < n)%N >-> m < n} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltnr : injective f -> - {homo f : m n / (n <= m)%N >-> m <= n} -> - {homo f : m n / (n < m)%N >-> m < n} := - inj_nhomo_lt (f := f). -Definition incnr_inj : - {mono f : m n / (m <= n)%N >-> m <= n} -> injective f := - inc_inj (f := f). -Definition decnr_inj : - {mono f : m n / (n <= m)%N >-> m <= n} -> injective f := - dec_inj (f := f). -Definition decnr_inj_inj := decnr_inj. -Definition lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} -> - {mono f : m n / (m < n)%N >-> m < n} := - leW_mono (f := f). -Definition lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} -> - {mono f : m n / (n < m)%N >-> m < n} := - leW_nmono (f := f). -Definition lenr_mono : {homo f : m n / (m < n)%N >-> m < n} -> - {mono f : m n / (m <= n)%N >-> m <= n} := - le_mono (f := f). -Definition lenr_nmono : - {homo f : m n / (n < m)%N >-> m < n} -> - {mono f : m n / (n <= m)%N >-> m <= n} := - le_nmono (f := f). -Definition ltnrW_homo_in : - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} := - ltW_homo_in (f := f). -Definition ltnrW_nhomo_in : - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} := - inj_nhomo_lt_in (f := f). -Definition incnr_inj_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decnr_inj_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition decnr_inj_inj_in := decnr_inj_in. -Definition lenrW_mono_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> - {in D &, {mono f : m n / (m < n)%N >-> m < n}} := - leW_mono_in (f := f). -Definition lenrW_nmono_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> - {in D &, {mono f : m n / (n < m)%N >-> m < n}} := - leW_nmono_in (f := f). -Definition lenr_mono_in : - {in D &, {homo f : m n / (m < n)%N >-> m < n}} -> - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} := - le_mono_in (f := f). -Definition lenr_nmono_in : - {in D &, {homo f : m n / (n < m)%N >-> m < n}} -> - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} := - le_nmono_in (f := f). -End NatToR. -Section RToNat. -Variables (D D' : pred R) (f : R -> nat). -Definition ltrnW_homo : - {homo f : m n / m < n >-> (m < n)%N} -> - {homo f : m n / m <= n >-> (m <= n)%N} := - ltW_homo (f := f). -Definition ltrnW_nhomo : - {homo f : m n / n < m >-> (m < n)%N} -> - {homo f : m n / n <= m >-> (m <= n)%N} := - ltW_nhomo (f := f). -Definition inj_homo_ltrn : injective f -> - {homo f : m n / m <= n >-> (m <= n)%N} -> - {homo f : m n / m < n >-> (m < n)%N} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltrn : injective f -> - {homo f : m n / n <= m >-> (m <= n)%N} -> - {homo f : m n / n < m >-> (m < n)%N} := - inj_nhomo_lt (f := f). -Definition incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f := - inc_inj (f := f). -Definition decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f := - dec_inj (f := f). -Definition lernW_mono : - {mono f : m n / m <= n >-> (m <= n)%N} -> - {mono f : m n / m < n >-> (m < n)%N} := - leW_mono (f := f). -Definition lernW_nmono : - {mono f : m n / n <= m >-> (m <= n)%N} -> - {mono f : m n / n < m >-> (m < n)%N} := - leW_nmono (f := f). -Definition ltrnW_homo_in : - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} := - ltW_homo_in (f := f). -Definition ltrnW_nhomo_in : - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} := - inj_nhomo_lt_in (f := f). -Definition incrn_inj_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decrn_inj_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lernW_mono_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> - {in D &, {mono f : m n / m < n >-> (m < n)%N}} := - leW_mono_in (f := f). -Definition lernW_nmono_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> - {in D &, {mono f : m n / n < m >-> (m < n)%N}} := - leW_nmono_in (f := f). -End RToNat. -End NumIntegralDomainMonotonyTheory. - -Section NumDomainOperationTheory. -Variable R : numDomainType. -Implicit Types x y z t : R. -Definition lerif_refl x C : reflect (x <= x ?= iff C) C := leif_refl. -Definition lerif_trans x1 x2 x3 C12 C23 : - x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23 := - @leif_trans _ _ x1 x2 x3 C12 C23. -Definition lerif_le x y : x <= y -> x <= y ?= iff (x >= y) := @leif_le _ _ x y. -Definition lerif_eq x y : x <= y -> x <= y ?= iff (x == y) := @leif_eq _ _ x y. -Definition ger_lerif x y C : x <= y ?= iff C -> (y <= x) = C := - @ge_leif _ _ x y C. -Definition ltr_lerif x y C : x <= y ?= iff C -> (x < y) = ~~ C := - @lt_leif _ _ x y C. -Definition normr_real x : `|x| \is real := normr_real x. -Definition ler_norm_sum I r (G : I -> R) (P : pred I): - `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i| := - ler_norm_sum r G P. -Definition ler_norm_sub x y : `|x - y| <= `|x| + `|y| := ler_norm_sub x y. -Definition ler_dist_add z x y : `|x - y| <= `|x - z| + `|z - y| := - ler_dist_add z x y. -Definition ler_sub_norm_add x y : `|x| - `|y| <= `|x + y| := - ler_sub_norm_add x y. -Definition ler_sub_dist x y : `|x| - `|y| <= `|x - y| := ler_sub_dist x y. -Definition ler_dist_dist x y : `| `|x| - `|y| | <= `|x - y| := - ler_dist_dist x y. -Definition ler_dist_norm_add x y : `| `|x| - `|y| | <= `|x + y| := - ler_dist_norm_add x y. -Definition ler_nnorml x y : y < 0 -> `|x| <= y = false := @ler_nnorml _ _ x y. -Definition ltr_nnorml x y : y <= 0 -> `|x| < y = false := @ltr_nnorml _ _ x y. -Definition lter_nnormr := (ler_nnorml, ltr_nnorml). -Definition mono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y / x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)} := - @mono_in_leif _ _ A f C. -Definition mono_lerif (f : R -> R) C : - {mono f : x y / x <= y} -> - forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C) := - @mono_leif _ _ f C. -Definition nmono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y /~ x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)} := - @nmono_in_leif _ _ A f C. -Definition nmono_lerif (f : R -> R) C : - {mono f : x y /~ x <= y} -> - forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C) := - @nmono_leif _ _ f C. -End NumDomainOperationTheory. - -Section RealDomainTheory. -Variable R : realDomainType. -Implicit Types x y z t : R. -Definition ler_total : total (@ler R) := le_total. -Definition ltr_total x y : x != y -> (x < y) || (y < x) := - @lt_total _ _ x y. -Definition wlog_ler P : - (forall a b, P b a -> P a b) -> (forall a b, a <= b -> P a b) -> - forall a b : R, P a b := - @wlog_le _ _ P. -Definition wlog_ltr P : - (forall a, P a a) -> - (forall a b, (P b a -> P a b)) -> (forall a b, a < b -> P a b) -> - forall a b : R, P a b := - @wlog_lt _ _ P. -Definition ltrNge x y : (x < y) = ~~ (y <= x) := @ltNge _ _ x y. -Definition lerNgt x y : (x <= y) = ~~ (y < x) := @leNgt _ _ x y. -Definition neqr_lt x y : (x != y) = (x < y) || (y < x) := @neq_lt _ _ x y. -Definition eqr_leLR x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t) := - @eq_leLR _ _ x y z t. -Definition eqr_leRL x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y) := - @eq_leRL _ _ x y z t. -Definition eqr_ltLR x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t) := - @eq_ltLR _ _ x y z t. -Definition eqr_ltRL x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y) := - @eq_ltRL _ _ x y z t. -End RealDomainTheory. - -Section RealDomainMonotony. -Variables (R : realDomainType) (R' : numDomainType) (D : pred R). -Variables (f : R -> R') (f' : R -> nat). -Definition ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y} := - le_mono (f := f). -Definition homo_mono := ler_mono. -Definition ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y} := - le_nmono (f := f). -Definition nhomo_mono := ler_nmono. -Definition ler_mono_in : - {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}} := - le_mono_in (f := f). -Definition homo_mono_in := ler_mono_in. -Definition ler_nmono_in : - {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}} := - le_nmono_in (f := f). -Definition nhomo_mono_in := ler_nmono_in. -Definition lern_mono : - {homo f' : m n / m < n >-> (m < n)%N} -> - {mono f' : m n / m <= n >-> (m <= n)%N} := - le_mono (f := f'). -Definition lern_nmono : - {homo f' : m n / n < m >-> (m < n)%N} -> - {mono f' : m n / n <= m >-> (m <= n)%N} := - le_nmono (f := f'). -Definition lern_mono_in : - {in D &, {homo f' : m n / m < n >-> (m < n)%N}} -> - {in D &, {mono f' : m n / m <= n >-> (m <= n)%N}} := - le_mono_in (f := f'). -Definition lern_nmono_in : - {in D &, {homo f' : m n / n < m >-> (m < n)%N}} -> - {in D &, {mono f' : m n / n <= m >-> (m <= n)%N}} := - le_nmono_in (f := f'). -End RealDomainMonotony. - -Section RealDomainOperations. -Variable R : realDomainType. -Implicit Types x y z : R. -Section MinMax. - -Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type. -Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed. -Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?]. -Ltac mexact x := by mapply x. - -Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. -Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. -Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. -Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed. -Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed. -Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed. -Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed. -Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed. - -Lemma minrA x y z : min x (min y z) = min (min x y) z. -Proof. mexact @minA. Qed. - -Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed. -Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed. -Lemma maxrA x y z : max x (max y z) = max (max x y) z. -Proof. mexact @maxA. Qed. - -Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed. -Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed. -Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed. -Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed. -Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed. -Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed. - -Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z). -Proof. mexact @le_minr. Qed. - -Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x). -Proof. mexact @le_minl. Qed. - -Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z). -Proof. mexact @le_maxr. Qed. - -Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x). -Proof. mexact @le_maxl. Qed. - -Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z). -Proof. mexact @lt_minr. Qed. - -Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x). -Proof. mexact @lt_minl. Qed. - -Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z). -Proof. mexact @lt_maxr. Qed. - -Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x). -Proof. mexact @lt_maxl. Qed. - -Definition lter_minr := (ler_minr, ltr_minr). -Definition lter_minl := (ler_minl, ltr_minl). -Definition lter_maxr := (ler_maxr, ltr_maxr). -Definition lter_maxl := (ler_maxl, ltr_maxl). - -Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed. -Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed. - -Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed. -Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed. -Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed. -Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed. - -Variant minr_spec x y : bool -> bool -> R -> Type := -| Minr_r of x <= y : minr_spec x y true false x -| Minr_l of y < x : minr_spec x y false true y. -Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y). -Proof. by rewrite mrE; case: leP; constructor. Qed. - -Variant maxr_spec x y : bool -> bool -> R -> Type := -| Maxr_r of y <= x : maxr_spec x y true false x -| Maxr_l of x < y : maxr_spec x y false true y. -Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y). -Proof. by rewrite mrE; case: (leP y); constructor. Qed. - -End MinMax. -End RealDomainOperations. - -Arguments lerifP {R x y C}. -Arguments lerif_refl {R x C}. -Arguments mono_in_lerif [R A f C]. -Arguments nmono_in_lerif [R A f C]. -Arguments mono_lerif [R f C]. -Arguments nmono_lerif [R f C]. - -Section RealDomainArgExtremum. - -Context {R : realDomainType} {I : finType} (i0 : I). -Context (P : pred I) (F : I -> R) (Pi0 : P i0). - -Definition arg_minr := extremum <=%R i0 P F. -Definition arg_maxr := extremum >=%R i0 P F. -Definition arg_minrP : extremum_spec <=%R P F arg_minr := arg_minP F Pi0. -Definition arg_maxrP : extremum_spec >=%R P F arg_maxr := arg_maxP F Pi0. - -End RealDomainArgExtremum. - -Notation "@ 'real_lerP'" := - (deprecate real_lerP real_leP) (at level 10, only parsing) : fun_scope. -Notation real_lerP := (@real_lerP _ _ _) (only parsing). -Notation "@ 'real_ltrP'" := - (deprecate real_ltrP real_ltP) (at level 10, only parsing) : fun_scope. -Notation real_ltrP := (@real_ltrP _ _ _) (only parsing). -Notation "@ 'real_ltrNge'" := - (deprecate real_ltrNge real_ltNge) (at level 10, only parsing) : fun_scope. -Notation real_ltrNge := (@real_ltrNge _ _ _) (only parsing). -Notation "@ 'real_lerNgt'" := - (deprecate real_lerNgt real_leNgt) (at level 10, only parsing) : fun_scope. -Notation real_lerNgt := (@real_lerNgt _ _ _) (only parsing). -Notation "@ 'real_ltrgtP'" := - (deprecate real_ltrgtP real_ltgtP) (at level 10, only parsing) : fun_scope. -Notation real_ltrgtP := (@real_ltrgtP _ _ _) (only parsing). -Notation "@ 'real_ger0P'" := - (deprecate real_ger0P real_ge0P) (at level 10, only parsing) : fun_scope. -Notation real_ger0P := (@real_ger0P _ _) (only parsing). -Notation "@ 'real_ltrgt0P'" := - (deprecate real_ltrgt0P real_ltgt0P) (at level 10, only parsing) : fun_scope. -Notation real_ltrgt0P := (@real_ltrgt0P _ _) (only parsing). -Notation lerif_nat := (deprecate lerif_nat leif_nat_r) (only parsing). -Notation "@ 'lerif_subLR'" := - (deprecate lerif_subLR leif_subLR) (at level 10, only parsing) : fun_scope. -Notation lerif_subLR := (@lerif_subLR _) (only parsing). -Notation "@ 'lerif_subRL'" := - (deprecate lerif_subRL leif_subRL) (at level 10, only parsing) : fun_scope. -Notation lerif_subRL := (@lerif_subRL _) (only parsing). -Notation "@ 'lerif_add'" := - (deprecate lerif_add leif_add) (at level 10, only parsing) : fun_scope. -Notation lerif_add := (@lerif_add _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_sum'" := - (deprecate lerif_sum leif_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_sum := (@lerif_sum _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_0_sum'" := - (deprecate lerif_0_sum leif_0_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_0_sum := (@lerif_0_sum _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_norm'" := - (deprecate real_lerif_norm real_leif_norm) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_norm := (@real_lerif_norm _ _) (only parsing). -Notation "@ 'lerif_pmul'" := - (deprecate lerif_pmul leif_pmul) (at level 10, only parsing) : fun_scope. -Notation lerif_pmul := (@lerif_pmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_nmul'" := - (deprecate lerif_nmul leif_nmul) (at level 10, only parsing) : fun_scope. -Notation lerif_nmul := (@lerif_nmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_pprod'" := - (deprecate lerif_pprod leif_pprod) (at level 10, only parsing) : fun_scope. -Notation lerif_pprod := (@lerif_pprod _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square_scaled'" := - (deprecate real_lerif_mean_square_scaled real_leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square_scaled := - (@real_lerif_mean_square_scaled _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2_scaled'" := - (deprecate real_lerif_AGM2_scaled real_leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2_scaled := - (@real_lerif_AGM2_scaled _ _ _) (only parsing). -Notation "@ 'lerif_AGM_scaled'" := - (deprecate lerif_AGM_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM_scaled := (@lerif_AGM_scaled _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square'" := - (deprecate real_lerif_mean_square real_leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square := - (@real_lerif_mean_square _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2'" := - (deprecate real_lerif_AGM2 real_leif_AGM2) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2 := (@real_lerif_AGM2 _ _ _) (only parsing). -Notation "@ 'lerif_AGM'" := - (deprecate lerif_AGM leif_AGM) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM := (@lerif_AGM _ _ _ _) (only parsing). -Notation "@ 'lerif_mean_square_scaled'" := - (deprecate lerif_mean_square_scaled leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square_scaled := - (@lerif_mean_square_scaled _) (only parsing). -Notation "@ 'lerif_AGM2_scaled'" := - (deprecate lerif_AGM2_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2_scaled := (@lerif_AGM2_scaled _) (only parsing). -Notation "@ 'lerif_mean_square'" := - (deprecate lerif_mean_square leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square := (@lerif_mean_square _) (only parsing). -Notation "@ 'lerif_AGM2'" := - (deprecate lerif_AGM2 leif_AGM2) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2 := (@lerif_AGM2 _) (only parsing). -Notation "@ 'lerif_normC_Re_Creal'" := - (deprecate lerif_normC_Re_Creal leif_normC_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_normC_Re_Creal := (@lerif_normC_Re_Creal _) (only parsing). -Notation "@ 'lerif_Re_Creal'" := - (deprecate lerif_Re_Creal leif_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_Re_Creal := (@lerif_Re_Creal _) (only parsing). -Notation "@ 'lerif_rootC_AGM'" := - (deprecate lerif_rootC_AGM leif_rootC_AGM) - (at level 10, only parsing) : fun_scope. -Notation lerif_rootC_AGM := (@lerif_rootC_AGM _ _ _ _) (only parsing). - -End Theory. - -Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" := - (arg_minr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" := - [arg minr_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" := - (arg_maxr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" := - [arg maxr_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope. - -End Num. -End mc_1_10. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 76bec6f..7875323 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -2049,6 +2049,5 @@ Qed. End Solver. -Notation "@ 'limg_add'" := - (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope. -Notation limg_add := (@limg_add _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use limgD instead.")] +Notation limg_add := limgD (only parsing). diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 17b1490..64863f4 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -2490,7 +2490,5 @@ Definition conj_cfMod := cfAutMod conjC. Definition conj_cfInd := cfAutInd conjC. Definition cfconjC_eq1 := cfAut_eq1 conjC. -Notation "@ 'cf_triangle_lerif'" := - (deprecate cf_triangle_lerif cf_triangle_leif) - (at level 10, only parsing). -Notation cf_triangle_lerif := (@cf_triangle_lerif _ _) (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use cf_triangle_leif instead.")] +Notation cf_triangle_lerif := cf_triangle_leif (only parsing). diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index dfcb5ac..9d01160 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -2732,6 +2732,7 @@ Arguments aut_groupAction {gT} G%g. Notation "[ 'Aut' G ]" := (aut_action G) : action_scope. Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope. -Notation pcycleE := (deprecate pcycleE porbitE _) (only parsing). -Notation pcycle_actperm := (deprecate pcycle_actperm porbit_actperm _) - (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbitE instead.")] +Notation pcycleE := porbitE (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit_actperm instead.")] +Notation pcycle_actperm := porbit_actperm (only parsing). diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 5775e34..a54d2a6 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -693,20 +693,27 @@ Qed. End CastSn. -Notation tuple_perm_eqP := - (deprecate tuple_perm_eqP tuple_permP) (only parsing). -Notation pcycle := (deprecate pcycle porbit _) (only parsing). -Notation pcycles := (deprecate pcycles porbits _) (only parsing). -Notation mem_pcycle := (deprecate mem_pcycle mem_porbit _) (only parsing). -Notation pcycle_id := (deprecate pcycle_id porbit_id _) (only parsing). -Notation uniq_traject_pcycle := - (deprecate uniq_traject_pcycle uniq_traject_porbit _) (only parsing). -Notation pcycle_traject := (deprecate pcycle_traject porbit_traject _) - (only parsing). -Notation iter_pcycle := (deprecate iter_pcycle iter_porbit _) (only parsing). -Notation eq_pcycle_mem := (deprecate eq_pcycle_mem eq_porbit_mem _) - (only parsing). -Notation pcycle_sym := (deprecate pcycle_sym porbit_sym _) (only parsing). -Notation pcycle_perm := (deprecate pcycle_perm porbit_perm _) (only parsing). -Notation ncycles_mul_tperm := (deprecate ncycles_mul_tperm porbits_mul_tperm _) - (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use tuple_permP instead.")] +Notation tuple_perm_eqP := tuple_permP (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit instead.")] +Notation pcycle := porbit (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbits instead.")] +Notation pcycles := porbits (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use mem_porbit instead.")] +Notation mem_pcycle := mem_porbit (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit_id instead.")] +Notation pcycle_id := porbit_id (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use uniq_traject_porbit instead.")] +Notation uniq_traject_pcycle := uniq_traject_porbit (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit_traject instead.")] +Notation pcycle_traject := porbit_traject (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use iter_porbit instead.")] +Notation iter_pcycle := iter_porbit (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use eq_porbit_mem instead.")] +Notation eq_pcycle_mem := eq_porbit_mem (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit_sym instead.")] +Notation pcycle_sym := porbit_sym (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbit_perm instead.")] +Notation pcycle_perm := porbit_perm (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use porbits_mul_tperm instead.")] +Notation ncycles_mul_tperm := porbits_mul_tperm (only parsing). diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index c1f420f..10c0849 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -453,12 +453,10 @@ Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA). End Theory. -Notation "@ 'mulm_addl'" := - (deprecate mulm_addl mulmDl) (at level 10, only parsing) : fun_scope. -Notation "@ 'mulm_addr'" := - (deprecate mulm_addr mulmDr) (at level 10, only parsing) : fun_scope. -Notation mulm_addl := (@mulm_addl _ _ _) (only parsing). -Notation mulm_addr := (@mulm_addr _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulmDl instead.")] +Notation mulm_addl := mulmDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mulmDr instead.")] +Notation mulm_addr := mulmDr (only parsing). End Theory. Include Theory. @@ -1991,14 +1989,9 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m : Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed. Arguments biggcdn_inf [I] i0 [P F m]. -Notation filter_index_enum := - ((fun _ => @deprecated_filter_index_enum _) - (deprecate filter_index_enum big_enumP)) (only parsing). - -Notation big_rmcond := - ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) - (deprecate big_rmcond big_rmcond_in)) (only parsing). - -Notation big_uncond_in := - ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) - (deprecate big_uncond_in big_rmcond_in)) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use big_enumP instead.")] +Notation filter_index_enum := deprecated_filter_index_enum (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use big_rmcond_in instead.")] +Notation big_rmcond := big_rmcond_in (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use big_rmcond_in instead.")] +Notation big_uncond_in := big_rmcond_in (only parsing). diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index ae46cd3..aca1a29 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -1041,11 +1041,11 @@ Qed. End Chinese. -Notation "@ 'coprime_expl'" := - (deprecate coprime_expl coprimeXl) (at level 10, only parsing) : fun_scope. -Notation "@ 'coprime_expr'" := - (deprecate coprime_expr coprimeXr) (at level 10, only parsing) : fun_scope. -Notation coprime_mull := (deprecate coprime_mull coprimeMl) (only parsing). -Notation coprime_mulr := (deprecate coprime_mulr coprimeMr) (only parsing). -Notation coprime_expl := (fun k => @coprime_expl k _ _) (only parsing). -Notation coprime_expr := (fun k => @coprime_expr k _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimeMl instead.")] +Notation coprime_mull := coprimeMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimeMr instead.")] +Notation coprime_mulr := coprimeMr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimeXl instead.")] +Notation coprime_expl := coprimeXl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use coprimeXr instead.")] +Notation coprime_expr := coprimeXr (only parsing). diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 027b5d4..f0e1f5e 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2357,9 +2357,7 @@ End Greatest. End SetFixpoint. -Notation mem_imset := - ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _) - (only parsing). -Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => - deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _) - (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use imset_f instead.")] +Notation mem_imset := imset_f (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use imset2_f instead.")] +Notation mem_imset2 := imset2_f (only parsing). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 9d2b6c0..4fc602c 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -917,8 +917,8 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed. End OpsTheory. -Notation disjoint_trans := - (deprecate disjoint_trans disjointWl _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use disjointWl instead.")] +Notation disjoint_trans := disjointWl (only parsing). Hint Resolve subxx_hint : core. @@ -1723,12 +1723,10 @@ End ArgMinMax. End Extrema. -Notation "@ 'arg_minP'" := - (deprecate arg_minP arg_minnP) (at level 10, only parsing) : fun_scope. -Notation arg_minP := (@arg_minP _ _ _) (only parsing). -Notation "@ 'arg_maxP'" := - (deprecate arg_maxP arg_maxnP) (at level 10, only parsing) : fun_scope. -Notation arg_maxP := (@arg_maxP _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use arg_minnP instead.")] +Notation arg_minP := arg_minnP (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use arg_maxnP instead.")] +Notation arg_maxP := arg_maxnP (only parsing). Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := (arg_min i0 (fun i => P%B) (fun i => F)) @@ -2352,5 +2350,7 @@ Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed. End SumFinType. -Notation bump_addl := (deprecate bump_addl bumpDl) (only parsing). -Notation unbump_addl := (deprecate unbump_addl unbumpDl) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use bumpDl instead.")] +Notation bump_addl := bumpDl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use unbumpDl instead.")] +Notation unbump_addl := unbumpDl (only parsing). diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 5032dfd..24fb6f2 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -3422,12 +3422,10 @@ Proof. exact: anti_mono_in. Qed. End POrderMonotonyTheory. -Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt lt_sorted_eq) - (at level 10, only parsing) : fun_scope. -Notation "@ 'eq_sorted_le'" := (deprecate eq_sorted_le le_sorted_eq) - (at level 10, only parsing) : fun_scope. -Notation eq_sorted_lt := (@eq_sorted_lt _ _ _ _) (only parsing). -Notation eq_sorted_le := (@eq_sorted_le _ _ _ _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use lt_sorted_eq instead.")] +Notation eq_sorted_lt := lt_sorted_eq (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use le_sorted_eq instead.")] +Notation eq_sorted_le := le_sorted_eq (only parsing). End POrderTheory. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index d5c9488..dd3e867 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1677,64 +1677,27 @@ End CycleArc. Prenex Implicits arc. -(* Deprecated in 1.12.0 *) - -Notation "@ 'eq_sorted'" := - (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope. -Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq) - (at level 10, only parsing) : fun_scope. -Notation "@ 'sorted_lt_nth'" := - (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) => - deprecate sorted_lt_nth sorted_ltn_nth leT_tr) - (at level 10, only parsing) : fun_scope. -Notation "@ 'sorted_le_nth'" := - (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) => - deprecate sorted_le_nth sorted_leq_nth leT_tr) - (at level 10, only parsing) : fun_scope. -Notation "@ 'ltn_index'" := - (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) => - deprecate ltn_index sorted_ltn_index leT_tr) - (at level 10, only parsing) : fun_scope. -Notation "@ 'leq_index'" := - (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) => - deprecate leq_index sorted_leq_index leT_tr) - (at level 10, only parsing) : fun_scope. -Notation "@ 'subseq_order_path'" := (deprecate subseq_order_path subseq_path) - (at level 10, only parsing) : fun_scope. - -Notation eq_sorted := - (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing). -Notation eq_sorted_irr := - (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing). -Notation sorted_lt_nth := - (fun leT_tr x0 => @sorted_lt_nth _ _ leT_tr x0 _) (only parsing). -Notation sorted_le_nth := - (fun leT_tr leT_refl x0 => @sorted_le_nth _ _ leT_tr leT_refl x0 _) - (only parsing). -Notation ltn_index := (fun leT_tr => @ltn_index _ _ leT_tr _) (only parsing). -Notation leq_index := - (fun leT_tr leT_refl => @leq_index _ _ leT_tr leT_refl _) (only parsing). -Notation subseq_order_path := - (fun leT_tr => @subseq_order_path _ _ leT_tr _ _ _) (only parsing). - -(* Deprecated in 1.13.0 *) - -Notation "@ 'sub_path_in'" := - (deprecate sub_path_in sub_in_path) (at level 10, only parsing) : fun_scope. -Notation "@ 'sub_cycle_in'" := - (deprecate sub_cycle_in sub_in_cycle) (at level 10, only parsing) : fun_scope. -Notation "@ 'sub_sorted_in'" := (deprecate sub_sorted_in sub_in_sorted) - (at level 10, only parsing) : fun_scope. -Notation "@ 'eq_path_in'" := - (deprecate eq_path_in eq_in_path) (at level 10, only parsing) : fun_scope. -Notation "@ 'eq_cycle_in'" := - (deprecate eq_cycle_in eq_in_cycle) (at level 10, only parsing) : fun_scope. - -Notation sub_path_in := - (fun ee' => @sub_path_in _ _ _ _ ee' _ _) (only parsing). -Notation sub_cycle_in := - (fun ee' => @sub_cycle_in _ _ _ _ ee' _) (only parsing). -Notation sub_sorted_in := - (fun ee' => @sub_sorted_in _ _ _ _ ee' _) (only parsing). -Notation eq_path_in := (fun ee' => @eq_path_in _ _ _ _ ee' _ _) (only parsing). -Notation eq_cycle_in := (fun ee' => @eq_cycle_in _ _ _ _ ee' _) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sorted_eq instead.")] +Notation eq_sorted := sorted_eq (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use irr_sorted_eq instead.")] +Notation eq_sorted_irr := irr_sorted_eq (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sorted_ltn_nth instead.")] +Notation sorted_lt_nth := sorted_ltn_nth (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sorted_leq_nth instead.")] +Notation sorted_le_nth := sorted_leq_nth (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sorted_ltn_index instead.")] +Notation ltn_index := sorted_ltn_index (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sorted_leq_index instead.")] +Notation leq_index := sorted_leq_index (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use subseq_path instead.")] +Notation subseq_order_path := subseq_path (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_path instead.")] +Notation sub_path_in := sub_in_path (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_cycle instead.")] +Notation sub_cycle_in := sub_in_cycle (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use sub_in_sorted instead.")] +Notation sub_sorted_in := sub_in_sorted (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use eq_in_path instead.")] +Notation eq_path_in := eq_in_path (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use eq_in_cycle instead.")] +Notation eq_cycle_in := eq_in_cycle (only parsing). diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index ee5b136..f94e0a1 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -1429,11 +1429,11 @@ apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //. by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord. Qed. -Notation "@ 'primes_mul'" := - (deprecate primes_mul primesM) (at level 10, only parsing) : fun_scope. -Notation "@ 'primes_exp'" := - (deprecate primes_exp primesX) (at level 10, only parsing) : fun_scope. -Notation primes_mul := (@primes_mul _ _) (only parsing). -Notation primes_exp := (fun m => @primes_exp m _) (only parsing). -Notation pnat_mul := (deprecate pnat_mul pnatM) (only parsing). -Notation pnat_exp := (deprecate pnat_exp pnatX) (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use primesM instead.")] +Notation primes_mul := primesM (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use primesX instead.")] +Notation primes_exp := primesX (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use pnatM instead.")] +Notation pnat_mul := pnatM (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use pnatX instead.")] +Notation pnat_exp := pnatX (only parsing). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 2d5c5b8..401903a 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -4040,38 +4040,43 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := Ltac tfae := do !apply: AllIffConj. (* Temporary backward compatibility. *) -Notation take_addn := (deprecate take_addn takeD _) (only parsing). -Notation rot_addn := (deprecate rot_addn rotD _) (only parsing). -Notation nseq_addn := (deprecate nseq_addn nseqD _) (only parsing). -Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _) - (only parsing). -Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _) - (only parsing). -Notation perm_eq_all := (deprecate perm_eq_all perm_all _ _ _) - (only parsing). -Notation perm_eq_small := (deprecate perm_eq_small perm_small_eq _ _ _) - (only parsing). -Notation perm_eq_nilP := (deprecate perm_eq_nilP perm_nilP) (only parsing). -Notation perm_eq_consP := (deprecate perm_eq_consP perm_consP) (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_rev instead.")] +Notation perm_eq_rev := perm_rev (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_flatten instead.")] +Notation perm_eq_flatten := perm_flatten (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_all instead.")] +Notation perm_eq_all := perm_all (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_small_eq instead.")] +Notation perm_eq_small := perm_small_eq (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_nilP instead.")] +Notation perm_eq_nilP := perm_nilP (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_consP instead.")] +Notation perm_eq_consP := perm_consP (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use uniq_min_size instead.")] Notation leq_size_perm := ((fun T s1 s2 Us1 ss12 les21 => - let: (Esz12, Es12) := - deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21 + let: (Esz12, Es12) := uniq_min_size T s1 s2 Us1 ss12 les21 in conj Es12 Esz12) _ _ _) (only parsing). -Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) - (only parsing). -Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). -Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) - (only parsing). -(* TODO: restore when Coq 8.10 is no longer supported *) -(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *) +#[deprecated(since="mathcomp 1.9.0", note="Use uniq_perm instead.")] +Notation uniq_perm_eq := uniq_perm (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_iotaP instead.")] +Notation perm_eq_iotaP := perm_iotaP (only parsing). +#[deprecated(since="mathcomp 1.9.0", note="Use perm_count_undup instead.")] +Notation perm_undup_count := perm_count_undup (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use takeD instead.")] +Notation take_addn := takeD (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use rotD instead.")] +Notation rot_addn := rotD (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use nseqD instead.")] +Notation nseq_addn := nseqD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_catr instead.")] +Notation allpairs_catr := mem_allpairs_catr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_consr instead.")] +Notation allpairs_consr := mem_allpairs_consr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use allpairs_rconsr instead.")] +Notation perm_allpairs_rconsr := allpairs_rconsr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use iotaDl instead.")] +Notation iota_addl := iotaDl (only parsing). +#[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] Notation iota_add := iotaD (only parsing). -Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). - -Notation allpairs_catr := - (deprecate allpairs_catr mem_allpairs_catr _ _ _) (only parsing). -Notation allpairs_consr := - (deprecate allpairs_consr mem_allpairs_consr _ _ _) (only parsing). -Notation perm_allpairs_rconsr := - (deprecate perm_allpairs_rconsr allpairs_rconsr _ _ _) (only parsing). diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index e1e1b71..faecce2 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -12,22 +12,6 @@ Global Set Bullet Behavior "None". (* Prop are canonical nonPropType instances. This is *) (* useful for applied views. *) (* --> This will become standard with the Coq v8.11 SSReflect core library. *) -(* deprecate old new == new, but warning that old is deprecated and new *) -(* should be used instead. *) -(* --> Usage: Notation old := (deprecate old new) (only parsing). *) -(* --> Caveat: deprecate old new only inherits new's maximal implicits; *) -(* on-demand implicits should be added after : (deprecate old new _). *) -(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *) -(* non-prenex implicits, use the idiom: *) -(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *) -(* _ _ ... _) (only printing). *) -(* where all the implicit a_i's occur first, and correspond to the *) -(* trailing _'s, making sure deprecate old new is fully applied and *) -(* there are _no implicits_ inside the (fun .. => ..) expression. This *) -(* is to avoid triggering a bug in SSReflect elaboration that is *) -(* triggered by such evars under binders. *) -(* Import Deprecation.Silent :: turn off deprecation warning messages. *) -(* Import Deprecation.Reject :: raise an error instead of only warning. *) (* *) (* Intro pattern ltac views: *) (* - top of the stack actions: *) @@ -95,6 +79,8 @@ Ltac flag old_id new_id := Module Exports. Arguments hide {T} u v /. Coercion hide : exposed >-> hidden. +#[deprecated(since="mathcomp 1.13.0", + note="Use the deprecated attribute instead.")] Notation deprecate old_id new_id := (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id) (only parsing). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 8dbfc73..ad00d14 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1974,78 +1974,26 @@ Ltac nat_congr := first symmetry end ]. -Module mc_1_10. - -Variant leq_xor_gtn m n : bool -> bool -> Set := - | LeqNotGtn of m <= n : leq_xor_gtn m n true false - | GtnNotLeq of n < m : leq_xor_gtn m n false true. - -Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m). -Proof. by case: leqP; constructor. Qed. - -Variant ltn_xor_geq m n : bool -> bool -> Set := - | LtnNotGeq of m < n : ltn_xor_geq m n false true - | GeqNotLtn of n <= m : ltn_xor_geq m n true false. - -Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n). -Proof. by case: ltnP; constructor. Qed. - -Variant eqn0_xor_gt0 n : bool -> bool -> Set := - | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false - | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true. - -Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). -Proof. by case: n; constructor. Qed. - -Variant compare_nat m n : - bool -> bool -> bool -> bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n false false false true false true - | CompareNatGt of m > n : compare_nat m n false false true false true false - | CompareNatEq of m = n : compare_nat m n true true true true false false. - -Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) - (m <= n) (n < m) (m < n). -Proof. by case: ltngtP; constructor. Qed. - -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). - -Notation "@ 'iter_add'" := - (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. -Notation "@ 'odd_opp'" := - (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. -Notation "@ 'sqrn_sub'" := - (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. -Notation iter_add := (@iterD _) (only parsing). -Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). -Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). -Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). -Notation minn_mull := (deprecate minn_mull minnMl) (only parsing). -Notation odd_opp := (@odd_opp _ _) (only parsing). -Notation odd_mul := (deprecate odd_mul oddM) (only parsing). -Notation odd_exp := (deprecate odd_exp oddX) (only parsing). -Notation sqrn_sub := (@sqrn_sub _ _) (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use oddD instead.")] +Notation odd_add := oddD (only parsing). +#[deprecated(since="mathcomp 1.11.0", note="Use oddB instead.")] +Notation odd_sub := oddB (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use iterD instead.")] +Notation iter_add := iterD (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use maxnMr instead.")] +Notation maxn_mulr := maxnMr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use maxnMl instead.")] +Notation maxn_mull := maxnMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use minnMr instead.")] +Notation minn_mulr := minnMr (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use minnMl instead.")] +Notation minn_mull := minnMl (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use oddN instead.")] +Notation odd_opp := oddN (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use oddM instead.")] +Notation odd_mul := oddM (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use oddX instead.")] +Notation odd_exp := oddX (only parsing). +#[deprecated(since="mathcomp 1.12.0", note="Use sqrnB instead.")] +Notation sqrn_sub := sqrnB (only parsing). |