diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 13 |
2 files changed, 5 insertions, 11 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4de594e..71cc9a9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -386,6 +386,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). constructors, the case `mask [::] s` can be dealt with using `mask0s` or explicit conversion. +- in `ssrnum.v`, fixed notations `@minr` and `@maxr` to point `Order.min` and + `Order.max` respectively. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 4bb7a5a..dce3ffd 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -129,15 +129,6 @@ Local Open Scope order_scope. Local Open Scope ring_scope. Import Order.TTheory GRing.Theory. -Reserved Notation "<= y" (at level 35). -Reserved Notation ">= y" (at level 35). -Reserved Notation "< y" (at level 35). -Reserved Notation "> y" (at level 35). -Reserved Notation "<= y :> T" (at level 35, y at next level). -Reserved Notation ">= y :> T" (at level 35, y at next level). -Reserved Notation "< y :> T" (at level 35, y at next level). -Reserved Notation "> y :> T" (at level 35, y at next level). - Fact ring_display : unit. Proof. exact: tt. Qed. Module Num. @@ -392,10 +383,10 @@ Notation comparabler := (@Order.comparable ring_display _) (only parsing). Notation "@ 'comparabler' R" := (@Order.comparable ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. Notation maxr := (@Order.max ring_display _). -Notation "@ 'maxr' R" := (@Order.join ring_display R) +Notation "@ 'maxr' R" := (@Order.max ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. Notation minr := (@Order.min ring_display _). -Notation "@ 'minr' R" := (@Order.meet ring_display R) +Notation "@ 'minr' R" := (@Order.min ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. Section Def. |