Fix notation modifiers and scopes

1 files changed, 72 insertions, 65 deletions

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index b3df199..36adce0 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -372,29 +372,29 @@ Definition normr (R : numDomainType) (T : normedZmodType R) : T -> R :=
 Arguments normr {R T} x.
 
 Notation ler := (@Order.le ring_display _) (only parsing).
-Notation "@ 'ler' R" :=
-  (@Order.le ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'ler' R" := (@Order.le ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation ltr := (@Order.lt ring_display _) (only parsing).
-Notation "@ 'ltr' R" :=
-  (@Order.lt ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'ltr' R" := (@Order.lt ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation ger := (@Order.ge ring_display _) (only parsing).
-Notation "@ 'ger' R" :=
-  (@Order.ge ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'ger' R" := (@Order.ge ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation gtr := (@Order.gt ring_display _) (only parsing).
-Notation "@ 'gtr' R" :=
-  (@Order.gt ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'gtr' R" := (@Order.gt ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation lerif := (@Order.leif ring_display _) (only parsing).
-Notation "@ 'lerif' R" :=
-  (@Order.leif ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'lerif' R" := (@Order.leif ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 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).
+Notation "@ 'comparabler' R" := (@Order.comparable ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 Notation maxr := (@Order.join ring_display _).
-Notation "@ 'maxr' R" :=
-  (@Order.join ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'maxr' R" := (@Order.join ring_display R)
+    (at level 10, R at level 8, only parsing) : fun_scope.
 Notation minr := (@Order.meet ring_display _).
-Notation "@ 'minr' R" :=
-  (@Order.meet ring_display R) (at level 10, R at level 8, only parsing).
+Notation "@ 'minr' R" := (@Order.meet ring_display R)
+  (at level 10, R at level 8, only parsing) : fun_scope.
 
 Section Def.
 Context {R : numDomainType}.
@@ -442,34 +442,34 @@ Import Def Keys.
 
 Notation "`| x |" := (norm x) : ring_scope.
 
-Notation "<=%R" := le : ring_scope.
-Notation ">=%R" := ge : ring_scope.
-Notation "<%R" := lt : ring_scope.
-Notation ">%R" := gt : ring_scope.
-Notation "<?=%R" := leif : ring_scope.
-Notation ">=<%R" := comparable : ring_scope.
-Notation "><%R" := (fun x y => ~~ (comparable x y)) : ring_scope.
+Notation "<=%R" := le : fun_scope.
+Notation ">=%R" := ge : fun_scope.
+Notation "<%R" := lt : fun_scope.
+Notation ">%R" := gt : fun_scope.
+Notation "<?=%R" := leif : fun_scope.
+Notation ">=<%R" := comparable : fun_scope.
+Notation "><%R" := (fun x y => ~~ (comparable x y)) : fun_scope.
 
 Notation "<= y" := (ge y) : ring_scope.
-Notation "<= y :> T" := (<= (y : T)) : ring_scope.
+Notation "<= y :> T" := (<= (y : T)) (only parsing) : ring_scope.
 Notation ">= y"  := (le y) : ring_scope.
-Notation ">= y :> T" := (>= (y : T)) : ring_scope.
+Notation ">= y :> T" := (>= (y : T)) (only parsing) : ring_scope.
 
 Notation "< y" := (gt y) : ring_scope.
-Notation "< y :> T" := (< (y : T)) : ring_scope.
+Notation "< y :> T" := (< (y : T)) (only parsing) : ring_scope.
 Notation "> y" := (lt y) : ring_scope.
-Notation "> y :> T" := (> (y : T)) : ring_scope.
+Notation "> y :> T" := (> (y : T)) (only parsing) : ring_scope.
 
 Notation ">=< y" := (comparable y) : ring_scope.
-Notation ">=< y :> T" := (>=< (y : T)) : ring_scope.
+Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope.
 
 Notation "x <= y" := (le x y) : ring_scope.
-Notation "x <= y :> T" := ((x : T) <= (y : T)) : ring_scope.
+Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ring_scope.
 Notation "x >= y" := (y <= x) (only parsing) : ring_scope.
 Notation "x >= y :> T" := ((x : T) >= (y : T)) (only parsing) : ring_scope.
 
 Notation "x < y"  := (lt x y) : ring_scope.
-Notation "x < y :> T" := ((x : T) < (y : T)) : ring_scope.
+Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : ring_scope.
 Notation "x > y"  := (y < x) (only parsing) : ring_scope.
 Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : ring_scope.
 
@@ -4705,8 +4705,8 @@ Record of_ := Mixin {
 
 Variable (m : of_).
 
-Local Notation "x <= y" := (le m x y).
-Local Notation "x < y" := (lt m x y).
+Local Notation "x <= y" := (le m x y) : ring_scope.
+Local Notation "x < y" := (lt m x y) : ring_scope.
 Local Notation "`| x |" := (norm m x) : ring_scope.
 
 Lemma ltrr x : x < x = false. Proof. by rewrite lt_def eqxx. Qed.
@@ -4844,8 +4844,8 @@ Record of_ := Mixin {
 
 Variable (m : of_).
 
-Local Notation "x <= y" := (le m x y).
-Local Notation "x < y" := (lt m x y).
+Local Notation "x <= y" := (le m x y) : ring_scope.
+Local Notation "x < y" := (lt m x y) : ring_scope.
 Local Notation "`| x |" := (norm m x) : ring_scope.
 
 Let le0N x : (0 <= - x) = (x <= 0). Proof. by rewrite -sub0r sub_ge0. Qed.
@@ -4934,8 +4934,8 @@ Record of_ := Mixin {
 
 Variable (m : of_).
 
-Local Notation "x < y" := (lt m x y).
-Local Notation "x <= y" := (le m x y).
+Local Notation "x < y" := (lt m x y) : ring_scope.
+Local Notation "x <= y" := (le m x y) : ring_scope.
 Local Notation "`| x |" := (norm m x) : ring_scope.
 
 Fact lt0N x : (- x < 0) = (0 < x).
@@ -5536,101 +5536,108 @@ 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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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).
+  (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.