Adapt to math-comp/math-comp#1110

theories/core/cp_minor.v

@@ -22,7 +22,7 @@ Hypothesis (conn_G : connected [set: G]).
 (** ** Collapsing Bags *)
 
 Lemma collapse_bags (U : {set G}) u0' (inU : u0' \in U) :
-  let T := U :|: ~: \bigcup_(x in U) bag U x in 
+  let T := U :|: ~: (\bigcup_(x in U) bag U x) in
   let G' := sgraph.induced T in 
   exists phi : G -> G',
     [/\ total_minor_map phi,

theories/core/digraph.v

@@ -1138,10 +1138,10 @@ Section Neighborhood_def.
 Variable G : diGraph.
 
 Definition open_neigh (u : G) := [set v | u -- v].
-Local Notation "N( x )" := (open_neigh x) (at level 0, x at level 99, format "N( x )").
+Local Notation "N( x )" := (open_neigh x) (at level 0, format "N( x )").
 
 Definition closed_neigh (u : G) := u |: N(u).
-Local Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99, format "N[ x ]").
+Local Notation "N[ x ]" := (closed_neigh x) (at level 0, format "N[ x ]").
 
 Definition dominates (u v : G) : bool := (u == v) || (u -- v).
 
@@ -1156,27 +1156,27 @@ End Neighborhood_def.
 Notation "x -*- y" := (dominates x y) (at level 30).
 
 Notation "N( x )" := (@open_neigh _ x) 
-   (at level 0, x at level 99, format "N( x )").
+   (at level 0, format "N( x )").
 Notation "N[ x ]" := (@closed_neigh _ x) 
-   (at level 0, x at level 99, format "N[ x ]").
+   (at level 0, format "N[ x ]").
 Notation "N( G ; x )" := (@open_neigh G x)
-   (at level 0, G at level 99, x at level 99, only parsing).
+   (at level 0, only parsing).
 Notation "N[ G ; x ]" := (@closed_neigh G x)
-   (at level 0, G at level 99, x at level 99, only parsing).
+   (at level 0, only parsing).
 
 Notation "NS( G ; D )" := (@open_neigh_set G D) 
-   (at level 0, G at level 99, D at level 99, only parsing).
+   (at level 0, only parsing).
 Notation "NS( D )" := (open_neigh_set D) 
-   (at level 0, D at level 99, format "NS( D )").
+   (at level 0, format "NS( D )").
 Notation "NS[ G ; D ]" := (@closed_neigh_set G D) 
-   (at level 0, G at level 99, D at level 99, only parsing).
+   (at level 0, only parsing).
 Notation "NS[ D ]" := (closed_neigh_set D) 
-   (at level 0, D at level 99, format "NS[ D ]").
+   (at level 0, format "NS[ D ]").
 
 Notation "N( G ; x )" := (@open_neigh G x)
-   (at level 0, G at level 99, x at level 99, format "N( G ; x )") : implicit_scope.
+   (at level 0, format "N( G ; x )") : implicit_scope.
 Notation "N[ G ; x ]" := (@closed_neigh G x)
-   (at level 0, G at level 99, x at level 99, format "N[ G ; x ]") : implicit_scope.
+   (at level 0, format "N[ G ; x ]") : implicit_scope.
 
 Section Basic_Facts_Neighborhoods.
 

theories/core/mgraph.v

@@ -293,8 +293,8 @@ Record iso (F G: graph): Type@{S} :=
         iso_d: edge F -> bool;
         iso_ihom: is_ihom iso_v iso_e iso_d }.
 Infix "≃" := iso (at level 79).
-Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'"). 
-Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'"). 
+Notation "h '.e'" := (iso_e h) (at level 1, left associativity, format "h '.e'").
+Notation "h '.d'" := (iso_d h) (at level 1, left associativity, format "h '.d'").
 Global Existing Instance iso_ihom.
 Global Instance iso_hom (F G : graph) (h : F ≃ G) : is_hom h h.e h.d. 
 Proof. exact: ihom_hom. Qed.
@@ -869,8 +869,8 @@ Notation merge_seq G l := (merge G (eqv_clot l)).
 Arguments iso {Lv Le}.
 Arguments iso_id {_ _ _}.
 Infix "≃" := iso (at level 79).
-Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'").
-Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'"). 
+Notation "h '.e'" := (iso_e h) (at level 1, left associativity, format "h '.e'").
+Notation "h '.d'" := (iso_d h) (at level 1, left associativity, format "h '.d'").
 
 Tactic Notation "Iso" uconstr(f) uconstr(g) uconstr(h) :=
   match goal with |- ?F ≃ ?G => refine (@Iso _ _ F G f g h _) end.

theories/core/open_confluence.v

@@ -430,7 +430,7 @@ Global Instance add_test_graph (G : pre_graph) {graph_G : is_graph G} x a :
 Proof. split => //=; apply graph_G. Qed.
 
 Notation "G [adt x <- a ]" := (add_test G x a) 
-   (at level 2, left associativity, format "G [adt  x  <-  a ]") : open_scope.
+   (at level 1, left associativity, format "G [adt  x  <-  a ]") : open_scope.
 
 
 Definition flip_edge (G : pre_graph) (e : ET) :=
@@ -1576,7 +1576,7 @@ Notation "G - E" := (remove_edges G E) : open_scope.
 Notation "G ∔ [ x , u , y ]" := (add_edge G x u y) (at level 20,left associativity) : open_scope.
 Notation "G ∔ [ e , x , u , y ]" := (add_edge' G e x u y) (at level 20,left associativity) : open_scope.
 Notation "G [adt x <- a ]" := (add_test G x a) 
-   (at level 2, left associativity, format "G [adt  x  <-  a ]") : open_scope.
+   (at level 1, left associativity, format "G [adt  x  <-  a ]") : open_scope.
 
 #[export]
 Hint Resolve in_vsetDV in_vsetDE in_vsetAV in_vsetAE in_vsetAV' : vset.

theories/core/preliminaries.v

@@ -534,7 +534,7 @@ Proof. by rewrite /update eqxx. Qed.
 
 End update.
 Definition updateE := (update_eq,update_neq).
-Notation "f [upd x := y ]" := (update f x y) (at level 2, left associativity, format "f [upd  x  :=  y ]").
+Notation "f [upd x := y ]" := (update f x y) (at level 1, left associativity, format "f [upd  x  :=  y ]").
 
 Lemma update_same (aT : eqType) (rT : Type) (f : aT -> rT) x a b : 
   f[upd x := a][upd x := b] =1 f[upd x := b].

theories/core/setoid_bigop.v

@@ -132,7 +132,7 @@ Notation "x ⊗ y" := (mon2 x y) (left associativity, at level 25).
 
 Lemma big_split I r (P : pred I) (F1 F2 : I -> X) :
   \big[*%M/1]_(i <- r | P i) (F1 i ⊗ F2 i) ≡
-  (\big[*%M/1]_(i <- r | P i) F1 i) ⊗ \big[*%M/1]_(i <- r | P i) F2 i.
+  (\big[*%M/1]_(i <- r | P i) F1 i) ⊗ (\big[*%M/1]_(i <- r | P i) F2 i).
 Proof.
   elim/big_rec3 : _ => [|i x y z Pi ->]; rewrite ?monU //.
   rewrite -!monA. apply: mon_eqv => //. by rewrite monA [_ ⊗ y]monC monA.
@@ -154,7 +154,7 @@ Qed.
 
 Lemma bigID (I:eqType) r (a P : pred I) (F : I -> X) :
   \big[*%M/1]_(i <- r | P i) F i ≡
-  (\big[*%M/1]_(i <- r | P i && a i) F i) ⊗ \big[*%M/1]_(i <- r | P i && ~~ a i) F i.
+  (\big[*%M/1]_(i <- r | P i && a i) F i) ⊗ (\big[*%M/1]_(i <- r | P i && ~~ a i) F i).
 Proof.
   rewrite !(@big_mkcond _ I r _ F) -big_split. 
   apply: eqv_bigr => i; case: (a i); by rewrite /= ?andbT ?andbF ?monU ?monUl.
@@ -163,7 +163,7 @@ Arguments bigID [I r] a P F.
 
 
 Lemma bigD1 (I : finType) j (P : pred I) (F : I -> X) : 
-  P j -> \big[*%M/1]_(i | P i) F i ≡ F j ⊗ \big[*%M/1]_(i | P i && (i != j)) F i.
+  P j -> \big[*%M/1]_(i | P i) F i ≡ F j ⊗ (\big[*%M/1]_(i | P i && (i != j)) F i).
 Proof.
   move=> Pj; rewrite (bigID (pred1 j)); apply mon_eqv => //.
   apply: big_pred1 => i /=. by rewrite /= andbC; case: eqP => // ->.