diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec
index 5e05aa9f81..fe3a468d32 100644
--- a/examples/MEE-CBC/FunctionalSpec.ec
+++ b/examples/MEE-CBC/FunctionalSpec.ec
@@ -466,7 +466,7 @@ phoare mee_encrypt_correct _mk _ek _p _c:
 proof.
   have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c
           = mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move.
-  rewrite dmap1E /preim /pred1 /=.
+  rewrite dmap1E /pred1 /=.
   proc; inline MAC.tag PRPc.PseudoRP.f.
   swap 6 -5 => //=; alias 2 iv = s.
   while (   0 <= i <= size (pad _p (hmac_sha256 _mk _p))
@@ -528,7 +528,7 @@ conseq (_: true ==> true) (_: _ ==> _)=> //=.
   rewrite (ler_asym (size p) (size (behead _c)) _);
     rewrite ?ge_szc_p ?le_szc_p // take_size => p_def.
   split.
-  + case: {-1}(unpad p) (eq_refl (unpad p))=> //= @/mee_cbc - [] m t.
+  + case: {-1}(unpad p) (eq_refl (unpad p))=> //= - [] m t.
     by rewrite /mee_dec /= -p_def=> -> /=.
   by rewrite /mee_dec -p_def /= => ->.
  proc; inline *; wp; while true (size c - i); auto =>/#.
diff --git a/examples/SchnorrPK.ec b/examples/SchnorrPK.ec
index c285347d8d..8110496083 100644
--- a/examples/SchnorrPK.ec
+++ b/examples/SchnorrPK.ec
@@ -126,7 +126,7 @@ section SchnorrPKSecurity.
     rewrite /R /R_DL; move => sigmarel.
     byphoare (_: h = x /\ w' = w ==> _) => //; rewrite sigmarel.
     proc; inline*; swap 3 -2; swap 8 -7.
-    wp; rewrite /snd /=; auto => &hr />.
+    auto=> &hr />.
     by rewrite dt_ll => /> *; algebra.
   qed.
 
diff --git a/examples/UC/dh_enc.ec b/examples/UC/dh_enc.ec
index 7be8234c89..ef2bd6d935 100644
--- a/examples/UC/dh_enc.ec
+++ b/examples/UC/dh_enc.ec
@@ -1028,7 +1028,7 @@ wp; call (_:
   + by move => *; inline *;auto => /#.
   (* Backdoor F2Auth *)
   move=> m2 p; inline *; auto => /> &1 &2.
-  rewrite /staterel /leak oget_some /unblock /kstp /rcv.
+  rewrite /staterel /leak oget_some /rcv.
   by case (FKE.st{2}.`kst) => /> /#.
 
 (* WRAP-UP CALL *)
@@ -1712,11 +1712,11 @@ call (_: invotp OTP.Initiator.p{1}
     sp 1 0; if{1}.
     (* STEP INITIATOR *)
     + sp 0 1; match{2}.
-      + by rcondf {1} 1; auto => /> &1;rewrite /invotp /kstp; smt().
-      + rcondt {1} 1; first by auto => /> &1;rewrite /invotp /kstp; smt().
-        by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp /kstp;smt().
-      + rcondt {1} 1; first by auto => /> &1;rewrite /invotp /kstp;smt().
-        by sp 1 0; match{1};  by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp /kstp;smt().
+      + by rcondf {1} 1; auto => /> &1;rewrite /invotp; smt().
+      + rcondt {1} 1; first by auto => /> &1;rewrite /invotp; smt().
+        by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp;smt().
+      + rcondt {1} 1; first by auto => /> &1;rewrite /invotp;smt().
+        by sp 1 0; match{1};  by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp;smt().
       + rcondt {2} 1; first by move => *; wp;skip;smt().
         if{1}.
         + seq 0 3 : (#pre /\  (oget (getl (oget lfa{2}))) = Ch_Init);
@@ -1769,7 +1769,7 @@ call (_: invotp OTP.Initiator.p{1}
         seq 0 3 : (#pre /\ (oget (getl (oget lfa{2}))) <> Ch_Init);
           first by wp;skip;smt().
         by match {2}; 1: (by exfalso => /#); auto => /#.
-      by rcondf{1} 1; [ by auto => /> &1;rewrite /invotp /kstp;smt()| by auto=> />].
+      by rcondf{1} 1; [ by auto => /> &1;rewrite /invotp;smt()| by auto=> />].
     (* STEP RESPONDER *)
     sp 0 1; match{2}; first 3 by auto;rewrite /invotp /#.
     + by rcondf{2} 1; auto; rewrite /invotp /#.
diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca
index b9050761eb..f7fc2bce47 100644
--- a/theories/algebra/DynMatrix.eca
+++ b/theories/algebra/DynMatrix.eca
@@ -1335,7 +1335,7 @@ qed.
 
 lemma mul_colmxc (v:vector) c: (colmx v) *^ vectc 1 c = c ** v.
 proof.
-rewrite eq_vectorP size_scalarv size_mulmxv /= /max 1:// => i bound.
+rewrite eq_vectorP size_scalarv size_mulmxv /= 1:// => i bound.
 rewrite get_scalarv get_mulmxv dotpE /= /max /=.
 by rewrite Big.BAdd.big_int1 /= get_vectc // mulrC.
 qed.
@@ -1826,7 +1826,7 @@ lemma dmatrix1E d m : mu1 (dmatrix d (rows m) (cols m)) m =
     BRM.bigi predT (fun j => mu1 d m.[i, j]) 0 (cols m)) 0 (rows m).
 proof.
 pose g (m: matrix) := mkseq (fun i => col m i) (cols m).
-rewrite (in_dmap1E_can _ _ g) /ofcols.
+rewrite (in_dmap1E_can _ _ g) 1,2:/ofcols.
 - rewrite /g eq_matrixP /= => i j bound.
   by rewrite get_offunm /= 1:/# nth_mkseq 1:/# get_col.
 - rewrite /g => y y_in <- /=.
@@ -1902,7 +1902,7 @@ proof.
 move => k_ge0; rewrite /dmatrix /ofcols ler_maxr // dlist1 dmap_comp /(\o).
 apply eq_dmap_in => v /size_dvector; rewrite ler_maxr //= => s_v.
 rewrite /colmx s_v; apply/eq_matrixP => /= i j [i_bound j_bound]. 
-by rewrite /ofcols !get_offunm /#.
+by rewrite !get_offunm /#.
 qed.
 
 lemma supp_dmatrix d m r c : 
diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec
index 7d65744eb0..24e064d754 100644
--- a/theories/algebra/PolyReduce.ec
+++ b/theories/algebra/PolyReduce.ec
@@ -67,7 +67,7 @@ proof.
 move=> p un_p; rewrite ideal_eq1P 1:&(idI) //; apply/negP.
 move/fun_ext => /(_ poly1); rewrite mem_idT /I mem_idgen1.
 case/eqT=> q /(congr1 deg); rewrite deg1 => /eq_sym.
-case: (q = poly0) => [->|nz_q]; first by rewrite /( * ) mul0r deg0.
+case: (q = poly0) => [->|nz_q]; first by rewrite mul0r deg0.
 rewrite degM_proper; 1: by rewrite lc_polyXnDC // mulr1 lc_eq0.
 rewrite deg_polyXnDC // -!addrA /= gtr_eqF //.
 by rewrite (_ : 1 = 1 + 0) 1:// ler_lt_add // deg_ge1.
@@ -126,7 +126,7 @@ proof. by rewrite /( ** ) !scalepE -2!mulE reprK. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma eqv_Xn : eqv (exp X n) (-poly1).
-proof.  rewrite eqv_sym /eqv /[-] opprK /I mem_idgen1_gen. qed.
+proof.  rewrite eqv_sym /eqv opprK /I mem_idgen1_gen. qed.
 
 (* -------------------------------------------------------------------- *)
 op reduce (p : poly) : poly =
@@ -165,7 +165,7 @@ rewrite {1}(polyE p) /reduce !PCA.big_seq &(eqv_sum) /=.
 move=> i /mem_range [rg_i _]; rewrite mulrC -scalepA.
 pose q := exp X (i %/ n * n) * exp X (i %% n).
 rewrite !scalepE &(eqvMl) &(eqv_trans q).
-- rewrite (_ : q = exp X i) // /q /( * ) -exprD_nneg // -?divz_eq //.
+- rewrite (_ : q = exp X i) // /q -exprD_nneg // -?divz_eq //.
   - by rewrite mulr_ge0 // divz_ge0.
   - by rewrite modz_ge0 gtr_eqF.
 apply/eqvMr; rewrite -polyCX ?divz_ge0 // (IntID.mulrC _ n).
@@ -192,7 +192,7 @@ split=> [eq_rd|eqv_pq].
 have @/eqv @/I: eqv (reduce p) (reduce q).
 - by rewrite !(eqv_reducel, eqv_reducer).
 case/mem_idgen1=> r /(congr1 deg); case: (r = poly0) => [->>|nz_r].
-- by rewrite /( * ) mul0r deg0 deg_eq0 subr_eq0 => ->.
+- by rewrite mul0r deg0 deg_eq0 subr_eq0 => ->.
 have: deg (reduce q - reduce p) <= n.
 - by rewrite &(ler_trans _ _ _ (degB _ _)) ler_maxrP !deg_reduce.
 rewrite degM_proper.
@@ -411,8 +411,8 @@ rewrite polyDE; pose c := (bigi _ _ _ _); have ->: c.[k] = Coeff.zeror.
   move=> i [/mem_range [ge0_i lt_in] @/predC1 ne_ik].
   by rewrite polyZE polyXnE // (eq_sym k i) ne_ik /= mulr0.
 rewrite addr0 polyZE polyXnE //= mulr1 (reducewE (2 * n)).
-- case: (p = poly0) => [->|nz_p]; first by rewrite /( * ) mul0r deg0 /#.
-  case: (q = poly0) => [->|nz_q]; first by rewrite /( * ) mulr0 deg0 /#.
+- case: (p = poly0) => [->|nz_p]; first by rewrite mul0r deg0 /#.
+  case: (q = poly0) => [->|nz_q]; first by rewrite mulr0 deg0 /#.
   apply: (ler_trans (deg p + deg q)); last first.
   - by rewrite (_ : 2 * n = n + n) 1:#ring ler_add &(deg_reduced).
   by rewrite &(ler_trans (deg (p * q) + 1)) ?ler_addl // &(degM_le).
diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec
index 872ab847cb..99ec64cb28 100644
--- a/theories/algebra/Ring.ec
+++ b/theories/algebra/Ring.ec
@@ -698,7 +698,7 @@ abstract theory ComRingDflInv.
 
   realize mulVr.
   proof.
-  move=> x ^ un_x [y ^ -> <-] @/invr_.
+  move=> x ^ un_x [y ^ -> <-].
   by have /= -> := choicebP _ x un_x.
   qed.
 
@@ -707,7 +707,7 @@ abstract theory ComRingDflInv.
 
   realize unitout.
   proof.
-  by move=> x; rewrite /unit_ negb_exists => /choiceb_dfl /(_ x).
+  by move=> x; rewrite negb_exists => /choiceb_dfl /(_ x).
   qed.
 end ComRingDflInv.
 
diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec
index 66437a0eb6..e8c6830e4b 100644
--- a/theories/crypto/assumptions/DHIES.ec
+++ b/theories/crypto/assumptions/DHIES.ec
@@ -79,7 +79,7 @@ theory DHIES.
     pkl = map (snd \o snd) kk =>
     menc pkl tag ptxt = dmap (mencDHIES tag ptxt kk) (List.map (snd \o snd)).
   proof.
-  rewrite /mencDHIES /menc /dlistmap /zipks /encDHIES /=.
+  rewrite /mencDHIES /menc /encDHIES /=.
   rewrite djoin_dmap.
   move=> ->; rewrite -map_comp /(\o) /=.
   congr; congr; apply fun_ext => x.
diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec
index da0ba6d614..e900f86b4b 100644
--- a/theories/distributions/DList.ec
+++ b/theories/distributions/DList.ec
@@ -326,7 +326,7 @@ rewrite -(dlet_dmap _ C (fun ds => dmap d (F ds))) -dlist_add ~-1:/#.
 rewrite -(dmap_dprodE _ _ (fun (xy : _ * _) => F xy.`1 xy.`2)) /F /=.
 rewrite dlistSr ~-1:/# /= !dmap_dprodE_swap /= &(in_eq_dlet) /=.
 move=> x _; rewrite -(dmap_comp h (fun xs => rcons xs x)); congr.
-apply: ih => @/k2; 2,3: by smt().
+apply: ih; 2,3: by smt().
 have ->: k1 + (n - (k1 + 1)) = n - 1 by ring.
 by have := inrgf 0 _; smt().
 qed.
diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec
index f4c8ddf94e..4c38054c29 100644
--- a/theories/distributions/Distr.ec
+++ b/theories/distributions/Distr.ec
@@ -2821,7 +2821,7 @@ pose F x := fun n : int => mass (df n) x.
 split=> @/mdlim /= [x|s uq_s].
 - case: (converge (F x))%RealSeq => [|/lim_Ncnv ->//].
   apply: (geC_lim_from 0) => n _.
-  by rewrite /s /F massE ge0_mu1.
+  by rewrite /F massE ge0_mu1.
 rewrite (@bigID _ _ (fun x => RealSeq.converge (F x))).
 rewrite addrC big1 -1:add0r.
 - by move=> x [_ @/predC] /lim_Ncnv /=; apply.
@@ -3411,11 +3411,11 @@ lemma Jensen_fin ['a] (d : 'a distr) f g :
   => (forall a b, convex g a b)
   => g (E d f) <= E d (g \o f).
 proof.
-move=> fin_d ll_d cvx_g; rewrite !fin_expE /(\o) //; pose s := to_seq _.
+move=> fin_d ll_d cvx_g; rewrite !fin_expE //; pose s := to_seq _.
 move: ll_d; rewrite /is_lossless weightE !(@sumE_fin _ s) ?uniq_to_seq //=.
 - by move=> a; rewrite -supportP mem_to_seq.
 move=> {fin_d}; case: s => [|i s]; first by rewrite BRA.big_nil.
-rewrite !BRA.big_consT /=.
+rewrite !BRA.big_consT /(\o) /=.
 elim: s (mu1 d i) (ge0_mu d (pred1 i)) (f i) => [|x s ih] l ge0_l v.
 - by rewrite !BRA.big_nil /= => ->.
 rewrite !BRA.big_consT /=; have := ge0_mu d (pred1 x).
diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec
index 2187bc3915..725160d0ca 100644
--- a/theories/prelude/Logic.ec
+++ b/theories/prelude/Logic.ec
@@ -692,7 +692,7 @@ proof. by move => [y fy] @/pinv; rewrite ifT; smt(choicebP). qed.
 
 lemma pcancel_pinv (f : 'a->'b): 
   injective f => pcancel f (pinv f).
-proof. by move => inj_f @/pcansel x; smt(pinv_inv). qed.
+proof. by move => inj_f x; smt(pinv_inv). qed.
 
 
 (* -------------------------------------------------------------------- *)