diff --git a/theories/core/checkpoint.v b/theories/core/checkpoint.v
index b3c6f4c..453254f 100644
--- a/theories/core/checkpoint.v
+++ b/theories/core/checkpoint.v
@@ -45,7 +45,7 @@ Section CheckPoints.
 
   Hypothesis G_conn' : connected [set: G].
   Let G_conn : forall x y:G, connect sedge x y.
-  Proof using G_conn'. exact: connectedTE. Qed.
+  Proof. clear -G_conn'. exact: connectedTE. Qed.
 
   Lemma cp_sym x y : cp x y = cp y x.
   Proof using.
diff --git a/theories/core/cp_minor.v b/theories/core/cp_minor.v
index d912003..02508f0 100644
--- a/theories/core/cp_minor.v
+++ b/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,
diff --git a/theories/core/digraph.v b/theories/core/digraph.v
index 339ea69..865d2b9 100644
--- a/theories/core/digraph.v
+++ b/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.
 
diff --git a/theories/core/mgraph.v b/theories/core/mgraph.v
index a5fc0da..2c013c2 100644
--- a/theories/core/mgraph.v
+++ b/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.
diff --git a/theories/core/open_confluence.v b/theories/core/open_confluence.v
index b0f6dec..621c999 100644
--- a/theories/core/open_confluence.v
+++ b/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.
diff --git a/theories/core/preliminaries.v b/theories/core/preliminaries.v
index 1cfb86e..37e485f 100644
--- a/theories/core/preliminaries.v
+++ b/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].
diff --git a/theories/core/setoid_bigop.v b/theories/core/setoid_bigop.v
index 7c3621c..0a83bbb 100644
--- a/theories/core/setoid_bigop.v
+++ 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 => // ->.
diff --git a/theories/planar/hmap_ops.v b/theories/planar/hmap_ops.v
index f5bea9b..2f6ad47 100644
--- a/theories/planar/hmap_ops.v
+++ b/theories/planar/hmap_ops.v
@@ -1103,14 +1103,14 @@ Definition del_node := Hypermap del_node_can3.
 Hypothesis plainG : plain G.
 
 Let NP x : reflect (cnode z x || cnode z (edge x)) (x \in N).
-Proof using plainG.
-apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
+Proof.
+clear -plainG; apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
   by case/orP; [exists x|exists (edge x); rewrite // -cedge1r].
 by rewrite plain_orbit // !inE => zy /pred2P [?|?]; subst y; rewrite zy.
 Qed.
 
 Let edgeN x : edge x \in N = (x \in N). 
-Proof using. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.
+Proof. clear. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.
 
 Lemma del_node_cnode (u v : del_node) : cnode u v = cnode (val u) (val v).
 Proof. by rewrite fconnect_frestrict fconnect_skip //; apply: valP. Qed.