Fix some notation levels w.r.t. Corelib

Author: hivert

classical/filter.v

@@ -211,19 +211,19 @@ Reserved Notation "'\near' x & y , P"
   (at level 200, x, y at level 99, P at level 200,
    format "'\near'  x  &  y ,  P", only parsing).
 (*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter'  'of'  x ]").*)
-Reserved Notation "F `=>` G" (at level 70, format "F  `=>`  G").
-Reserved Notation "F --> G" (at level 70, format "F  -->  G").
+Reserved Notation "F `=>` G" (at level 55, format "F  `=>`  G").
+Reserved Notation "F --> G" (at level 55, format "F  -->  G").
 Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim'  F  'in'  T ]").
 Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg'  F  'in'  T ]").
 Reserved Notation "x \is_near F" (at level 10, format "x  \is_near  F").
 Reserved Notation "E @[ x --> F ]"
   (at level 60, x name, format "E  @[ x  -->  F ]").
 Reserved Notation "E @[ x \oo ]"
   (at level 60, x name, format "E  @[ x  \oo ]").
-Reserved Notation "f @ F" (at level 60, format "f  @  F").
+Reserved Notation "f @ F" (at level 50, format "f  @  F").
 Reserved Notation "E `@[ x --> F ]"
   (at level 60, x name, format "E  `@[ x  -->  F ]").
-Reserved Notation "f `@ F" (at level 60, format "f  `@  F").
+Reserved Notation "f `@ F" (at level 50, format "f  `@  F").
 
 HB.mixin Record isFiltered U T := {
   nbhs : T -> set_system U

theories/topology_theory/function_spaces.v

@@ -90,27 +90,27 @@ From mathcomp Require Import product_topology.
 (******************************************************************************)
 
 Reserved Notation "{ 'uniform`' A -> V }"
-  (at level 0, A at level 69, format "{ 'uniform`'  A  ->  V }").
+  (at level 0, A at level 49, format "{ 'uniform`'  A  ->  V }").
 Reserved Notation "{ 'uniform' U -> V }"
-  (at level 0, U at level 69, format "{ 'uniform'  U  ->  V }").
+  (at level 0, U at level 49, format "{ 'uniform'  U  ->  V }").
 Reserved Notation "{ 'uniform' A , F --> f }"
-  (at level 0, A at level 69, F at level 69,
+  (at level 0, A at level 49, F at level 69,
    format "{ 'uniform'  A ,  F  -->  f }").
 Reserved Notation "{ 'uniform' , F --> f }"
-  (at level 0, F at level 69,
+  (at level 0, F at level 49,
    format "{ 'uniform' ,  F  -->  f }").
 Reserved Notation "{ 'ptws' U -> V }"
-  (at level 0, U at level 69, format "{ 'ptws'  U  ->  V }").
+  (at level 0, U at level 49, format "{ 'ptws'  U  ->  V }").
 Reserved Notation "{ 'ptws' , F --> f }"
-  (at level 0, F at level 69, format "{ 'ptws' ,  F  -->  f }").
+  (at level 0, F at level 49, format "{ 'ptws' ,  F  -->  f }").
 Reserved Notation "{ 'family' fam , U -> V }"
-  (at level 0, U at level 69, format "{ 'family'  fam ,  U  ->  V }").
+  (at level 0, U at level 49, format "{ 'family'  fam ,  U  ->  V }").
 Reserved Notation "{ 'family' fam , F --> f }"
-  (at level 0, F at level 69, format "{ 'family'  fam ,  F  -->  f }").
+  (at level 0, F at level 49, format "{ 'family'  fam ,  F  -->  f }").
 Reserved Notation "{ 'compact-open' , U -> V }"
-  (at level 0, U at level 69, format "{ 'compact-open' ,  U  ->  V }").
+  (at level 0, U at level 49, format "{ 'compact-open' ,  U  ->  V }").
 Reserved Notation "{ 'compact-open' , F --> f }"
-  (at level 0, F at level 69, format "{ 'compact-open' ,  F  -->  f }").
+  (at level 0, F at level 49, format "{ 'compact-open' ,  F  -->  f }").
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.