Fix notation modifiers and scopes

2 files changed, 143 insertions, 136 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.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 84a3430..572c9ae 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -963,34 +963,34 @@ Arguments gt {_ _}.
 
 Module Import POSyntax.
 
-Notation "<=%O" := le : order_scope.
-Notation ">=%O" := ge : order_scope.
-Notation "<%O" := lt : order_scope.
-Notation ">%O" := gt : order_scope.
-Notation "<?=%O" := leif : order_scope.
-Notation ">=<%O" := comparable : order_scope.
-Notation "><%O" := (fun x y => ~~ (comparable x y)) : order_scope.
+Notation "<=%O" := le : fun_scope.
+Notation ">=%O" := ge : fun_scope.
+Notation "<%O" := lt : fun_scope.
+Notation ">%O" := gt : fun_scope.
+Notation "<?=%O" := leif : fun_scope.
+Notation ">=<%O" := comparable : fun_scope.
+Notation "><%O" := (fun x y => ~~ (comparable x y)) : fun_scope.
 
 Notation "<= y" := (ge y) : order_scope.
-Notation "<= y :> T" := (<= (y : T)) : order_scope.
+Notation "<= y :> T" := (<= (y : T)) (only parsing) : order_scope.
 Notation ">= y"  := (le y) : order_scope.
-Notation ">= y :> T" := (>= (y : T)) : order_scope.
+Notation ">= y :> T" := (>= (y : T)) (only parsing) : order_scope.
 
 Notation "< y" := (gt y) : order_scope.
-Notation "< y :> T" := (< (y : T)) : order_scope.
+Notation "< y :> T" := (< (y : T)) (only parsing) : order_scope.
 Notation "> y" := (lt y) : order_scope.
-Notation "> y :> T" := (> (y : T)) : order_scope.
+Notation "> y :> T" := (> (y : T)) (only parsing) : order_scope.
 
 Notation ">=< y" := (comparable y) : order_scope.
-Notation ">=< y :> T" := (>=< (y : T)) : order_scope.
+Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : order_scope.
 
 Notation "x <= y" := (le x y) : order_scope.
-Notation "x <= y :> T" := ((x : T) <= (y : T)) : order_scope.
+Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : order_scope.
 Notation "x >= y" := (y <= x) (only parsing) : order_scope.
 Notation "x >= y :> T" := ((x : T) >= (y : T)) (only parsing) : order_scope.
 
 Notation "x < y"  := (lt x y) : order_scope.
-Notation "x < y :> T" := ((x : T) < (y : T)) : order_scope.
+Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : order_scope.
 Notation "x > y"  := (y < x) (only parsing) : order_scope.
 Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : order_scope.
 
@@ -1618,10 +1618,10 @@ Fact total_display : unit. Proof. exact: tt. Qed.
 
 Notation max := (@join total_display _).
 Notation "@ 'max' T" :=
-  (@join total_display T) (at level 10, T at level 8, only parsing).
+  (@join total_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 Notation min := (@meet total_display _).
 Notation "@ 'min' T" :=
-  (@meet total_display T) (at level 10, T at level 8, only parsing).
+  (@meet total_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 
 Notation "\max_ ( i <- r | P ) F" :=
   (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope.
@@ -2067,36 +2067,36 @@ Local Notation "T ^c" := (converse T) (at level 2, format "T ^c") : type_scope.
 
 Module Import ConverseSyntax.
 
-Notation "<=^c%O" := (@le (converse_display _) _) : order_scope.
-Notation ">=^c%O" := (@ge (converse_display _) _)  : order_scope.
-Notation ">=^c%O" := (@ge (converse_display _) _)  : order_scope.
-Notation "<^c%O" := (@lt (converse_display _) _) : order_scope.
-Notation ">^c%O" := (@gt (converse_display _) _) : order_scope.
-Notation "<?=^c%O" := (@leif (converse_display _) _) : order_scope.
-Notation ">=<^c%O" := (@comparable (converse_display _) _) : order_scope.
+Notation "<=^c%O" := (@le (converse_display _) _) : fun_scope.
+Notation ">=^c%O" := (@ge (converse_display _) _)  : fun_scope.
+Notation ">=^c%O" := (@ge (converse_display _) _)  : fun_scope.
+Notation "<^c%O" := (@lt (converse_display _) _) : fun_scope.
+Notation ">^c%O" := (@gt (converse_display _) _) : fun_scope.
+Notation "<?=^c%O" := (@leif (converse_display _) _) : fun_scope.
+Notation ">=<^c%O" := (@comparable (converse_display _) _) : fun_scope.
 Notation "><^c%O" := (fun x y => ~~ (@comparable (converse_display _) _ x y)) :
-  order_scope.
+  fun_scope.
 
 Notation "<=^c y" := (>=^c%O y) : order_scope.
-Notation "<=^c y :> T" := (<=^c (y : T)) : order_scope.
+Notation "<=^c y :> T" := (<=^c (y : T)) (only parsing) : order_scope.
 Notation ">=^c y"  := (<=^c%O y) : order_scope.
-Notation ">=^c y :> T" := (>=^c (y : T)) : order_scope.
+Notation ">=^c y :> T" := (>=^c (y : T)) (only parsing) : order_scope.
 
 Notation "<^c y" := (>^c%O y) : order_scope.
-Notation "<^c y :> T" := (<^c (y : T)) : order_scope.
+Notation "<^c y :> T" := (<^c (y : T)) (only parsing) : order_scope.
 Notation ">^c y" := (<^c%O y) : order_scope.
-Notation ">^c y :> T" := (>^c (y : T)) : order_scope.
+Notation ">^c y :> T" := (>^c (y : T)) (only parsing) : order_scope.
 
 Notation ">=<^c y" := (>=<^c%O y) : order_scope.
-Notation ">=<^c y :> T" := (>=<^c (y : T)) : order_scope.
+Notation ">=<^c y :> T" := (>=<^c (y : T)) (only parsing) : order_scope.
 
 Notation "x <=^c y" := (<=^c%O x y) : order_scope.
-Notation "x <=^c y :> T" := ((x : T) <=^c (y : T)) : order_scope.
+Notation "x <=^c y :> T" := ((x : T) <=^c (y : T)) (only parsing) : order_scope.
 Notation "x >=^c y" := (y <=^c x) (only parsing) : order_scope.
 Notation "x >=^c y :> T" := ((x : T) >=^c (y : T)) (only parsing) : order_scope.
 
 Notation "x <^c y"  := (<^c%O x y) : order_scope.
-Notation "x <^c y :> T" := ((x : T) <^c (y : T)) : order_scope.
+Notation "x <^c y :> T" := ((x : T) <^c (y : T)) (only parsing) : order_scope.
 Notation "x >^c y"  := (y <^c x) (only parsing) : order_scope.
 Notation "x >^c y :> T" := ((x : T) >^c (y : T)) (only parsing) : order_scope.
 
@@ -4042,20 +4042,20 @@ Module DvdSyntax.
 
 Notation dvd := (@le dvd_display _).
 Notation "@ 'dvd' T" :=
-  (@le dvd_display T) (at level 10, T at level 8, only parsing).
+  (@le dvd_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 Notation sdvd := (@lt dvd_display _).
 Notation "@ 'sdvd' T" :=
-  (@lt dvd_display T) (at level 10, T at level 8, only parsing).
+  (@lt dvd_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 
 Notation "x %| y" := (dvd x y) : order_scope.
 Notation "x %<| y" := (sdvd x y) : order_scope.
 
 Notation gcd := (@meet dvd_display _).
 Notation "@ 'gcd' T" :=
-  (@meet dvd_display T) (at level 10, T at level 8, only parsing).
+  (@meet dvd_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 Notation lcm := (@join dvd_display _).
 Notation "@ 'lcm' T" :=
-  (@join dvd_display T) (at level 10, T at level 8, only parsing).
+  (@join dvd_display T) (at level 10, T at level 8, only parsing) : fun_scope.
 
 Notation nat0 := (@top dvd_display _).
 Notation nat1 := (@bottom dvd_display _).
@@ -4281,36 +4281,36 @@ Fact prod_display : unit. Proof. by []. Qed.
 
 Module Import ProdSyntax.
 
-Notation "<=^p%O" := (@le prod_display _) : order_scope.
-Notation ">=^p%O" := (@ge prod_display _)  : order_scope.
-Notation ">=^p%O" := (@ge prod_display _)  : order_scope.
-Notation "<^p%O" := (@lt prod_display _) : order_scope.
-Notation ">^p%O" := (@gt prod_display _) : order_scope.
-Notation "<?=^p%O" := (@leif prod_display _) : order_scope.
-Notation ">=<^p%O" := (@comparable prod_display _) : order_scope.
+Notation "<=^p%O" := (@le prod_display _) : fun_scope.
+Notation ">=^p%O" := (@ge prod_display _)  : fun_scope.
+Notation ">=^p%O" := (@ge prod_display _)  : fun_scope.
+Notation "<^p%O" := (@lt prod_display _) : fun_scope.
+Notation ">^p%O" := (@gt prod_display _) : fun_scope.
+Notation "<?=^p%O" := (@leif prod_display _) : fun_scope.
+Notation ">=<^p%O" := (@comparable prod_display _) : fun_scope.
 Notation "><^p%O" := (fun x y => ~~ (@comparable prod_display _ x y)) :
-  order_scope.
+  fun_scope.
 
 Notation "<=^p y" := (>=^p%O y) : order_scope.
-Notation "<=^p y :> T" := (<=^p (y : T)) : order_scope.
+Notation "<=^p y :> T" := (<=^p (y : T)) (only parsing) : order_scope.
 Notation ">=^p y"  := (<=^p%O y) : order_scope.
-Notation ">=^p y :> T" := (>=^p (y : T)) : order_scope.
+Notation ">=^p y :> T" := (>=^p (y : T)) (only parsing) : order_scope.
 
 Notation "<^p y" := (>^p%O y) : order_scope.
-Notation "<^p y :> T" := (<^p (y : T)) : order_scope.
+Notation "<^p y :> T" := (<^p (y : T)) (only parsing) : order_scope.
 Notation ">^p y" := (<^p%O y) : order_scope.
-Notation ">^p y :> T" := (>^p (y : T)) : order_scope.
+Notation ">^p y :> T" := (>^p (y : T)) (only parsing) : order_scope.
 
 Notation ">=<^p y" := (>=<^p%O y) : order_scope.
-Notation ">=<^p y :> T" := (>=<^p (y : T)) : order_scope.
+Notation ">=<^p y :> T" := (>=<^p (y : T)) (only parsing) : order_scope.
 
 Notation "x <=^p y" := (<=^p%O x y) : order_scope.
-Notation "x <=^p y :> T" := ((x : T) <=^p (y : T)) : order_scope.
+Notation "x <=^p y :> T" := ((x : T) <=^p (y : T)) (only parsing) : order_scope.
 Notation "x >=^p y" := (y <=^p x) (only parsing) : order_scope.
 Notation "x >=^p y :> T" := ((x : T) >=^p (y : T)) (only parsing) : order_scope.
 
 Notation "x <^p y"  := (<^p%O x y) : order_scope.
-Notation "x <^p y :> T" := ((x : T) <^p (y : T)) : order_scope.
+Notation "x <^p y :> T" := ((x : T) <^p (y : T)) (only parsing) : order_scope.
 Notation "x >^p y"  := (y <^p x) (only parsing) : order_scope.
 Notation "x >^p y :> T" := ((x : T) >^p (y : T)) (only parsing) : order_scope.
 
@@ -4394,36 +4394,36 @@ Fact lexi_display : unit. Proof. by []. Qed.
 
 Module Import LexiSyntax.
 
-Notation "<=^l%O" := (@le lexi_display _) : order_scope.
-Notation ">=^l%O" := (@ge lexi_display _) : order_scope.
-Notation ">=^l%O" := (@ge lexi_display _) : order_scope.
-Notation "<^l%O" := (@lt lexi_display _) : order_scope.
-Notation ">^l%O" := (@gt lexi_display _) : order_scope.
-Notation "<?=^l%O" := (@leif lexi_display _) : order_scope.
-Notation ">=<^l%O" := (@comparable lexi_display _) : order_scope.
+Notation "<=^l%O" := (@le lexi_display _) : fun_scope.
+Notation ">=^l%O" := (@ge lexi_display _) : fun_scope.
+Notation ">=^l%O" := (@ge lexi_display _) : fun_scope.
+Notation "<^l%O" := (@lt lexi_display _) : fun_scope.
+Notation ">^l%O" := (@gt lexi_display _) : fun_scope.
+Notation "<?=^l%O" := (@leif lexi_display _) : fun_scope.
+Notation ">=<^l%O" := (@comparable lexi_display _) : fun_scope.
 Notation "><^l%O" := (fun x y => ~~ (@comparable lexi_display _ x y)) :
-  order_scope.
+  fun_scope.
 
 Notation "<=^l y" := (>=^l%O y) : order_scope.
-Notation "<=^l y :> T" := (<=^l (y : T)) : order_scope.
+Notation "<=^l y :> T" := (<=^l (y : T)) (only parsing) : order_scope.
 Notation ">=^l y"  := (<=^l%O y) : order_scope.
-Notation ">=^l y :> T" := (>=^l (y : T)) : order_scope.
+Notation ">=^l y :> T" := (>=^l (y : T)) (only parsing) : order_scope.
 
 Notation "<^l y" := (>^l%O y) : order_scope.
-Notation "<^l y :> T" := (<^l (y : T)) : order_scope.
+Notation "<^l y :> T" := (<^l (y : T)) (only parsing) : order_scope.
 Notation ">^l y" := (<^l%O y) : order_scope.
-Notation ">^l y :> T" := (>^l (y : T)) : order_scope.
+Notation ">^l y :> T" := (>^l (y : T)) (only parsing) : order_scope.
 
 Notation ">=<^l y" := (>=<^l%O y) : order_scope.
-Notation ">=<^l y :> T" := (>=<^l (y : T)) : order_scope.
+Notation ">=<^l y :> T" := (>=<^l (y : T)) (only parsing) : order_scope.
 
 Notation "x <=^l y" := (<=^l%O x y) : order_scope.
-Notation "x <=^l y :> T" := ((x : T) <=^l (y : T)) : order_scope.
+Notation "x <=^l y :> T" := ((x : T) <=^l (y : T)) (only parsing) : order_scope.
 Notation "x >=^l y" := (y <=^l x) (only parsing) : order_scope.
 Notation "x >=^l y :> T" := ((x : T) >=^l (y : T)) (only parsing) : order_scope.
 
 Notation "x <^l y"  := (<^l%O x y) : order_scope.
-Notation "x <^l y :> T" := ((x : T) <^l (y : T)) : order_scope.
+Notation "x <^l y :> T" := ((x : T) <^l (y : T)) (only parsing) : order_scope.
 Notation "x >^l y"  := (y <^l x) (only parsing) : order_scope.
 Notation "x >^l y :> T" := ((x : T) >^l (y : T)) (only parsing) : order_scope.
 
@@ -4681,9 +4681,9 @@ End ProdOrder.
 Module Exports.
 
 Notation "T *prod[ d ] T'" := (type d T T')
-  (at level 70, d at next level, format "T  *prod[ d ]  T'") : order_scope.
+  (at level 70, d at next level, format "T  *prod[ d ]  T'") : type_scope.
 Notation "T *p T'" := (type prod_display T T')
-  (at level 70, format "T  *p  T'") : order_scope.
+  (at level 70, format "T  *p  T'") : type_scope.
 
 Canonical eqType.
 Canonical choiceType.
@@ -5009,9 +5009,9 @@ End ProdLexiOrder.
 Module Exports.
 
 Notation "T *lexi[ d ] T'" := (type d T T')
-  (at level 70, d at next level, format "T  *lexi[ d ]  T'") : order_scope.
+  (at level 70, d at next level, format "T  *lexi[ d ]  T'") : type_scope.
 Notation "T *l T'" := (type lexi_display T T')
-  (at level 70, format "T  *l  T'") : order_scope.
+  (at level 70, format "T  *l  T'") : type_scope.
 
 Canonical eqType.
 Canonical choiceType.
@@ -5634,9 +5634,9 @@ Module Exports.
 
 Notation "n .-tupleprod[ disp ]" := (type disp n)
   (at level 2, disp at next level, format "n .-tupleprod[ disp ]") :
-  order_scope.
+  type_scope.
 Notation "n .-tupleprod" := (n.-tupleprod[prod_display])
-  (at level 2, format "n .-tupleprod") : order_scope.
+  (at level 2, format "n .-tupleprod") : type_scope.
 
 Canonical eqType.
 Canonical choiceType.