From 7f0699b6a6fa8486c21b292ba2d8a8910c37dd6b Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 11:46:43 +0900 Subject: Remove `Reserved Notation`s in `ssrnum.v` which are already declared in `order.v` --- mathcomp/algebra/ssrnum.v | 9 --------- 1 file changed, 9 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 4bb7a5a..553e9cf 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. -- cgit v1.2.3 From 0cadfe448ecb17a55d256d1c1a4470a95beab640 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 11:47:21 +0900 Subject: Fix `@maxr` and `@minr` --- mathcomp/algebra/ssrnum.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 553e9cf..dce3ffd 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -383,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. -- cgit v1.2.3