diff options
| author | Kazuhiko Sakaguchi | 2020-11-20 11:47:21 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-24 02:19:53 +0900 |
| commit | 0cadfe448ecb17a55d256d1c1a4470a95beab640 (patch) | |
| tree | ba2fc9780f041e546c67a5650a854332009ac394 /mathcomp | |
| parent | 7f0699b6a6fa8486c21b292ba2d8a8910c37dd6b (diff) | |
Fix `@maxr` and `@minr`
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |