running semi-automated linting on the whole library

7 files changed, 115 insertions, 115 deletions

diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v
index 48adbb3..54cb1c5 100644
--- a/mathcomp/attic/algnum_basic.v
+++ b/mathcomp/attic/algnum_basic.v
@@ -102,12 +102,12 @@ pose g := fun l => let p := minPoly K l in \prod_(i < size p) f p`_i; exists g =
 pose p := minPoly K l; pose n := (size p).-1.
 pose s := mkseq (fun i => p`_i * (g l) ^+ (n - i)%N) (size p).
 have kI (i : 'I_(size p)) : p`_i \in K by apply/all_nthP => //; apply/minPolyOver.
-have glA : g l \in A by rewrite/g; elim/big_ind: _ => // i _; apply/fHa.
+have glA : g l \in A by rewrite /g; elim/big_ind: _ => // i _; apply/fHa.
 have pmon: p`_n = 1 by have /monicP := monic_minPoly K l.
-have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly. 
+have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly.
 have eqPs: (Poly s) = s :> seq L0.
   by rewrite (PolyK (c := 0)) // -nth_last size_mkseq an1 oner_neq0.
-have ilen i : i < size p -> i <= n by move => iB; rewrite /n -ltnS prednK // size_minPoly.
+have ilen i : i < size p -> i <= n by move=> iB; rewrite /n -ltnS prednK // size_minPoly.
 split => //; first by apply/prodf_neq0 => i _.
 exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // size_mkseq an1.
   rewrite /root -(mulr0 ((g l) ^+ n)); have <- := minPolyxx K l.
@@ -116,11 +116,11 @@ exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // si
   by congr (_ * _); rewrite -exprD subnK ?ilen.
 apply/(all_nthP 0) => i; rewrite eqPs size_mkseq => iB; rewrite nth_mkseq //.
   have := ilen _ iB; rewrite leq_eqVlt => /orP.
-  case; first by move /eqP ->; rewrite subnn pmon mulr1.
+  case; first by move/eqP ->; rewrite subnn pmon mulr1.
   rewrite -subn_gt0 => {pmon ilen eqPs an1} /prednK <-; rewrite exprS mulrA /= Amcl ?rpredX //.
   rewrite /g (bigD1 (Ordinal iB)) //= mulrA; apply/Amcl.
     by rewrite mulrC; apply/fHk/(kI (Ordinal iB)).
-  by rewrite rpred_prod => // j _; apply/fHa. 
+  by rewrite rpred_prod => // j _; apply/fHa.
 Qed.
 
 Lemma int_clos_incl a : a \in A -> integral a.
@@ -135,7 +135,7 @@ Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r ->
 Proof.
 have Aaddr : addr_closed A := Asubr; have Amulr : mulr_closed A := Asubr.
 have Aoppr : oppr_closed A := Asubr; have [Aid _ _] := Asubr.
-move => rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s).
+move=> rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s).
 pose f j := sval (g j); pose fH j := svalP (g j).
 pose M := \matrix_(i, j < size r) f j (tnth s i).
 exists (char_poly M); rewrite char_poly_monic; split => //.
@@ -153,7 +153,7 @@ Qed.
 Lemma intPr l : integral l -> exists r : seq L0,
   [/\ r != nil, all A r & \sum_(i < size r) r`_i * l ^+ i = l ^+ (size r)].
 Proof.
-move => [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p).
+move=> [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p).
 have ps : n > 1.
   rewrite ltnNge; apply/negP => /size1_polyC pc; rewrite pc in pr pm => {pc}.
   move: pr => /rootP; rewrite hornerC => pc0.
@@ -163,10 +163,10 @@ exists r; split.
   apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred.
   by rewrite -subn1 subn_eq0 leqNgt ps.
   have : - p \is a polyOver A by rewrite rpredN //; apply Asubr.
-  by move => /allP-popA; apply/allP => x /mem_take /popA.
+  by move=> /allP-popA; apply/allP => x /mem_take /popA.
 move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW.
 rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP.
-rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //.    
+rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //.
 by rewrite coefN mulNr.
 Qed.
 
@@ -174,11 +174,11 @@ Lemma int_subring_closed a b : integral a -> integral b ->
   integral (a - b) /\ integral (a * b).
 Proof.
 have [A0 _ ] := (Asubr : zmod_closed A); have [A1 Asubr2 Amulr2] := Asubr.
-move => /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]].
+move=> /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]].
 pose n := size ra; pose m := size rb; pose r := Finite.enum [finType of 'I_n * 'I_m].
 pose G (z : 'I_n * 'I_m) := let (k, l) := z in a ^ k * b ^l.
 have [nz mz] : 0 < n /\ 0 < m.
-  by rewrite !lt0n; split; apply/negP; move => /nilP/eqP; rewrite ?ran ?rbn.
+  by rewrite !lt0n; split; apply/negP => - /nilP/eqP; rewrite ?ran ?rbn.
 have rnn : has (fun x => G x != 0) r.
   apply/hasP; exists (Ordinal nz, Ordinal mz); first by rewrite /r -enumT mem_enum.
   by rewrite /G mulr1 oner_neq0.
@@ -186,22 +186,22 @@ pose h s i : 'I_(size s) -> L0 := fun k => if (i != size s) then (i == k)%:R els
 pose f i j (z : 'I_n * 'I_m) : L0 := let (k, l) := z in h ra i k * h rb j l.
 have fA i j : forall z, f i j z \in A.
   have hA s k l : all A s -> h s k l \in A.
-    move => /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->].
-      by apply/sa/mem_nth. 
+    move=> /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->].
+      by apply/sa/mem_nth.
     by case (eqVneq k l) => [/eqP ->|/negbTE ->].
-  by move => [k l]; rewrite /f; apply/Amulr2; apply/hA.
+  by move=> [k l]; rewrite /f; apply/Amulr2; apply/hA.
 have fS i j : (i <= n) -> (j <= m) -> \sum_(z <- r) f i j z * G z = a ^ i * b ^ j.
   have hS s k c : (k <= size s) -> \sum_(l < size s) s`_l * c ^ l = c ^ (size s) ->
     \sum_(l < size s) h s k l * c ^ l = c ^ k.
-    move => kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx.
+    move=> kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx.
     rewrite kn; rewrite leq_eqVlt (negbTE kn) /= in kB => {kn}.
     rewrite (bigD1 (Ordinal kB)) //= eqxx mul1r /= -[RHS]addr0; congr (_ + _).
     by apply/big1 => l; rewrite eq_sym => kl; have : k != l := kl => /negbTE ->; rewrite mul0r.
-  move => iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml.
+  move=> iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml.
   rewrite (eq_bigr (fun k => \sum_(l < m) (h ra i k * a ^ k) * (h rb j l * b ^ l))).
     rewrite pair_bigA; apply eq_bigr => [[k l] _]; rewrite !mulrA; congr (_ * _).
     by rewrite -!mulrA [in h rb j l * a ^ k] mulrC.
-  by move => k _; rewrite mulr_sumr.
+  by move=> k _; rewrite mulr_sumr.
 pose fB i j z := f i.+1 j z - f i j.+1 z; pose fM i j z := f i.+1 j.+1 z.
 have fBA i j z : fB i j z \in A by rewrite /fB Asubr2.
 have fBM i j z : fM i j z \in A by rewrite /fM.
@@ -213,10 +213,10 @@ by rewrite /fM [in RHS]/G mulrA [in (a * b) * a ^ i] mulrC mulrA -exprSr -mulrA
 Qed.
 
 Lemma int_zmod_closed a b : integral a -> integral b -> integral (a - b).
-Proof. by move => aI bI; have [Azmod] := int_subring_closed aI bI. Qed.
+Proof. by move=> aI bI; have [Azmod] := int_subring_closed aI bI. Qed.
 
 Lemma int_mulr_closed a b : integral a -> integral b -> integral (a * b).
-Proof. by move => aI bI; have [_] := int_subring_closed aI bI. Qed.
+Proof. by move=> aI bI; have [_] := int_subring_closed aI bI. Qed.
 
 End Integral.
 
@@ -233,7 +233,7 @@ Definition tr : L0 -> L0 -> F := fun l k =>
 
 Fact tr_is_scalar l : scalar (tr l).
 Proof.
-move => c a b; rewrite /tr  -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE.
+move=> c a b; rewrite /tr  -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE.
 by rewrite mulrDr mulrDl linearD /= -scalerAr -scalerAl linearZ.
 Qed.
 
@@ -241,7 +241,7 @@ Canonical tr_additive l := Additive (@tr_is_scalar l).
 Canonical tr_linear l := AddLinear (@tr_is_scalar l).
   
 Lemma tr_sym : commutative tr.
-Proof. by move => a b; rewrite /tr mulrC. Qed.
+Proof. by move=> a b; rewrite /tr mulrC. Qed.
 
 Hypothesis Asubr : subring_closed A.
 Hypothesis Aint  : int_closed A.
@@ -267,36 +267,36 @@ Lemma dual_basis_def :
   forall (i : 'I_m), tr X`_i Y`_i = 1 /\
   forall (j : 'I_m), j != i -> tr X`_i Y`_j = 0}.
 Proof.
-pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0}); 
+pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0});
 pose HomV := [vectType _ of 'Hom(Uv, Fv)].
 pose tr_sub : Uv -> Uv -> Fv := fun u v => (tr (vsval u) (vsval v))%:A.
 have HomVdim : \dim {:HomV} = m by rewrite dimvf /Vector.dim /= /Vector.dim /= dimv1 muln1.
 have [f fH] : {f : 'Hom(Uv, HomV) | forall u, f u =1 tr_sub u}.
-  have lf1 u : linear (tr_sub u) by move => c x y; rewrite /tr_sub linearP scalerDl scalerA.
+  have lf1 u : linear (tr_sub u) by move=> c x y; rewrite /tr_sub linearP scalerDl scalerA.
   have lf2 : linear (fun u => linfun (Linear (lf1 u))).
-    move => c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub.
+    move=> c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub.
     by rewrite tr_sym linearP scalerDl scalerA /=; congr (_ + _); rewrite tr_sym.
   by exists (linfun (Linear lf2)) => u v; rewrite !lfunE.
 have [Xdual XdualH] : {Xdual : m.-tuple HomV |
   forall (i : 'I_m) u, Xdual`_i u = (coord X i (vsval u))%:A}.
   have lg (i : 'I_m) : linear (fun u : Uv => (coord X i (vsval u))%:A : Fv).
-    by move => c x y; rewrite linearP /= scalerDl scalerA.
+    by move=> c x y; rewrite linearP /= scalerDl scalerA.
   exists (mktuple (fun i => linfun (Linear (lg i)))) => i u.
   by rewrite -tnth_nth tnth_mktuple !lfunE.
 have [finv finvH] : {finv : 'Hom(HomV, L0) | finv =1 vsval \o (f^-1)%VF}.
-  by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE. 
+  by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE.
 pose Y := map_tuple finv Xdual; exists Y => Und Xb.
 have Ydef (i : 'I_m) : Y`_i = finv Xdual`_i by rewrite -!tnth_nth tnth_map.
 have XiU (i : 'I_m) : X`_i \in U by apply/(basis_mem Xb)/mem_nth; rewrite size_tuple.
 have Xii (i : 'I_m) : coord X i X`_i = 1%:R.
   by rewrite coord_free ?eqxx //; apply (basis_free Xb).
 have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R.
-  by rewrite coord_free; [move => /negbTE -> | apply (basis_free Xb)].
+  by rewrite coord_free; [move=> /negbTE -> | apply (basis_free Xb)].
 have Xdualb : basis_of fullv Xdual.
   suffices Xdualf : free Xdual.
     rewrite /basis_of Xdualf andbC /= -dimv_leqif_eq ?subvf // eq_sym HomVdim.
     by move: Xdualf; rewrite /free => /eqP => ->; rewrite size_tuple.
-  apply/freeP => k sX i.  
+  apply/freeP => k sX i.
   suffices: (\sum_(i < m) k i *: Xdual`_i) (vsproj U X`_i) = (k i)%:A.
     by rewrite sX zero_lfunE => /esym /eqP; rewrite scaler_eq0 oner_eq0 orbF => /eqP.
   rewrite sum_lfunE (bigD1 i) //= scale_lfunE XdualH vsprojK // Xii.
@@ -311,10 +311,10 @@ have flimg : limg f = fullv.
   apply/eqP; rewrite -dimv_leqif_eq ?subvf // limg_dim_eq; last by rewrite finj capv0.
   by rewrite HomVdim dimvf /Vector.dim.
 have finvK : cancel finv (f \o vsproj U).
-  by move => u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf.
+  by move=> u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf.
 have finv_inj : (lker finv = 0)%VS by apply/eqP/lker0P/(can_inj finvK).
-have finv_limg : limg finv = U. 
-  apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0.   
+have finv_limg : limg finv = U.
+  apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0.
   by apply/subvP => u /memv_imgP [h _] ->; rewrite finvH subvsP.
 have Xt (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = (tr Y`_j X`_i)%:A.
   by rewrite fH /tr_sub !vsprojK // Ydef finvH subvsP.
@@ -355,7 +355,7 @@ Definition trK : L0 -> L0 -> K' := tr (aspaceOver K L).
 Lemma trK_ndeg (U : {aspace L0}) : (K <= U)%VS ->
   (ndeg trK U <-> ndeg (tr (aspaceOver K L)) (aspaceOver K U)).
 Proof.
-move => UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL.
+move=> UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL.
 split => [ndK l lnz | nd l lnz].
   by rewrite UU' => liU; have [k] := ndK l lnz liU; exists k; rewrite UU'.
 by rewrite -UU' => liU'; have [k] := nd l lnz liU'; exists k; rewrite -UU'.
@@ -397,8 +397,8 @@ Lemma int_mod_closed : module (int_closure A L).
 Proof.
 have [A0 _] : zmod_closed A := Asubr; split.
   by rewrite /int_closure mem0v; split => //; apply/int_clos_incl.
-move => a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL.
-by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl. 
+move=> a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL.
+by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl.
 Qed.
 
 End Modules.
@@ -408,7 +408,7 @@ Variable (F0 : fieldType) (E : fieldExtType F0) (I : pred E) (Ifr K : {subfield
 Hypothesis Isubr : subring_closed I.
 Hypothesis Iint : int_closed I.
 Hypothesis Ipid : PID I.
-Hypothesis Ifrac : is_frac_field I Ifr. 
+Hypothesis Ifrac : is_frac_field I Ifr.
 Hypothesis IsubK : {subset I <= K}.
 Hypothesis Knd :  ndeg (trK Ifr K) K.
 
@@ -422,24 +422,24 @@ suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield
   have Ifrsub : (Ifr <= K)%VS.
     apply/subvP=> x /fHk-[fHx fHxx]; rewrite -(mulKf (fH0 x) x).
     by apply/memvM; rewrite ?memvV; apply/IsubK.
-  have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg. 
+  have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg.
   have Ifrac1 : is_frac_field (I : pred L0) 1.
-    split; first by move => a; rewrite /= trivial_fieldOver; apply/Isub.
+    split; first by move=> a; rewrite /= trivial_fieldOver; apply/Isub.
     by exists f => k; split => //; rewrite trivial_fieldOver => /fHk.
   have [X Xsize [Xf [Xs Xi]]] := FisK _ L0 _ _ Isubr Iint Ipid Ifrac1 Lnd.
   rewrite -dim_aspaceOver => //; have /eqP <- := Xsize; exists (in_tuple X); split; last first.
-    split => m; last by move => /Xi; rewrite /int_closure LK.  
-    by rewrite /int_closure -LK; move => /Xs.
-  move: Xf; rewrite -{1}(in_tupleE X); move => /freeP-XfL0; apply/freeP => k.
+    split => m; last by move=> /Xi; rewrite /int_closure LK.
+    by rewrite /int_closure -LK => - /Xs.
+  move: Xf; rewrite -{1}(in_tupleE X) => - /freeP-XfL0; apply/freeP => k.
   have [k' kk'] : exists k' : 'I_(size X) -> F, forall i, (k i)%:A = vsval (k' i).
     by exists (fun i => vsproj Ifr (k i)%:A) => i; rewrite vsprojK ?rpredZ ?mem1v.
   pose Ainj := fmorph_inj [rmorphism of in_alg E].
-  move => kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP.
+  move=> kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP.
   rewrite raddf_eq0; last by apply/subvs_inj.
   by apply/eqP/XfL0; rewrite -{3}kS => {i}; apply/eq_bigr => i _; rewrite -[RHS]mulr_algl kk'.
-move => Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
+move=> Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
 have [A0 _] : zmod_closed A := Asubr; have [Asub1 _] := Afrac1.
-have AsubL : {subset A <= L} by move => a /Asub1; apply (subvP (sub1v L) a).
+have AsubL : {subset A <= L} by move=> a /Asub1; apply (subvP (sub1v L) a).
 have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
   forall i : 'I_n, integral A b1`_i].
   pose b0 := vbasis L; have [f /all_and3-[fH0 fHa fHi]] := frac_field_alg_int Asubr Afrac1.
@@ -453,7 +453,7 @@ have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
     have dinA : d \in A by rewrite rpred_prod.
     rewrite limg_amulr; apply/eqP; rewrite -dimv_leqif_eq; first by rewrite dim_cosetv_unit.
     by apply/prodv_sub => //; apply/AsubL.
-  rewrite -lim limg_basis_of //; last by apply/vbasisP. 
+  rewrite -lim limg_basis_of //; last by apply/vbasisP.
   by have /eqP -> := lker0_amulr dun; rewrite capv0.
 have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L b2 &
   forall b, b \in L -> integral A b -> forall i, (coord b2 i b)%:A \in A].
@@ -465,55 +465,55 @@ have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L
   by congr (_ + _); apply/big1 => j jneqi; rewrite (oj j jneqi) mulr0.
 have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A X) ->
   exists B, basis_of_mod A M B.
-  move: k X M; elim => [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms].
-    by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0. 
+  move: k X M; elim=> [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms].
+    by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0.
   pose X1 := [tuple of behead X]; pose v := thead X.
   pose M1 := fun m => M m /\ coord X ord0 m = 0.
   pose M2 := fun (a : L0) => exists2 m, M m & (coord X ord0 m)%:A = a.
   have scr r m : r \in A -> exists c, r * m = c *: m.
-    by move => /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl.
+    by move=> /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl.
   have span_coord m : M m -> exists r : (k.+1).-tuple L0,
     [/\ all A r, m = \sum_(i < k.+1) r`_i * X`_i & forall i, (coord X i m)%:A = r`_i].
     have seqF (s : seq L0) : all A s -> exists s', s = [seq c%:A | c <- s'].
       elim: s => [_| a l IHl /= /andP[/Asub1/vlineP[c ->]]]; first by exists [::].
-      by move => /IHl[s' ->]; exists (c :: s').
-    move => mM; have := Ms m mM; rewrite /span_mod !size_tuple; move => [r rA rS].
+      by move=> /IHl[s' ->]; exists (c :: s').
+    move=> mM; have := Ms m mM; rewrite /span_mod !size_tuple => - [r rA rS].
     exists r; split => //; have [rF rFr] := seqF r rA => {seqF}; rewrite rFr in rA.
     have rFs : size rF = k.+1 by rewrite -(size_tuple r) rFr size_map.
     have -> : m = \sum_(i < k.+1) rF`_i *: X`_i.
       by rewrite rS; apply/eq_bigr => i _; rewrite rFr (nth_map 0) ?rFs // mulr_algl.
-    by move => i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs. 
+    by move=> i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs.
   have [B1 [B1f [B1s B1A]]] : exists B1, basis_of_mod A M1 B1.
     have X1f : free X1 by move: Xf; rewrite (tuple_eta X) free_cons => /andP[_].
     apply/(IH X1) => //.
       rewrite /module /M1 linear0; split => // a x y aA [xM xfc0] [yM yfc0].
       have := Mm a x y aA xM yM; move: aA => /Asub1/vlineP[r] ->; rewrite mulr_algl => msc.
       by rewrite /M1 linearB linearZ /= xfc0 yfc0 subr0 mulr0.
-    move => m [mM mfc0]; have := span_coord m mM; move => [r [rA rS rC]].
-    move: mfc0 (rC 0) ->; rewrite scale0r; move => r0; rewrite /span_mod size_tuple.
+    move=> m [mM mfc0]; have := span_coord m mM => - [r [rA rS rC]].
+    move: mfc0 (rC 0) ->; rewrite scale0r => - r0; rewrite /span_mod size_tuple.
     exists [tuple of behead r]; first by apply/allP => a /mem_behead/(allP rA).
     by rewrite rS big_ord_recl -r0 mul0r add0r; apply/eq_bigr => i _; rewrite !nth_behead.
   have [a [w wM wC] aG] : exists2 a, M2 a & forall v, M2 v -> exists2 d, d \in A & d * a = v.
     apply/Apid; split.
-      move => c [m mM <-]; have := span_coord m mM; move => [r [/all_nthP-rA _ rC]].
+      move=> c [m mM <-]; have := span_coord m mM => - [r [/all_nthP-rA _ rC]].
       by move: rC ->; apply/rA; rewrite size_tuple.
     split; first by exists 0 => //; rewrite linear0 scale0r.
-    move => c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM. 
+    move=> c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM.
     move: cA => /Asub1/vlineP[r] ->; rewrite !mulr_algl => mC.
     by exists (r *: mx - my) => //; rewrite linearB linearZ /= scalerBl -scalerA mxC myC.
   pose Ainj := fmorph_inj [rmorphism of in_alg L0].
   have mcM1 m : M m -> exists2 d, d \in A & d * a = (coord X 0 m)%:A.
-    by move => mM; apply/aG; exists m.
+    by move=> mM; apply/aG; exists m.
   case: (eqVneq a 0) => [| an0].
-    exists B1; split => //; split => [m mM |]; last by move => m /B1A[mM].
+    exists B1; split => //; split => [m mM |]; last by move=> m /B1A[mM].
     apply/B1s; split => //; apply/Ainj => /=; have [d _ <-] := mcM1 m mM.
-    by rewrite a0 mulr0 scale0r.      
+    by rewrite a0 mulr0 scale0r.
   exists (w :: B1); split.
     rewrite free_cons B1f andbT; move: an0; apply/contra; move: wC <-.
-    rewrite -(in_tupleE B1); move => /coord_span ->; apply/eqP.
+    rewrite -(in_tupleE B1) => - /coord_span ->; apply/eqP.
     rewrite linear_sum big1 ?scale0r => //= i _; rewrite linearZ /=.
     by have [_] := B1A B1`_i (mem_nth 0 (ltn_ord _)) => ->; rewrite mulr0.
-  split => [m mM | m]; last by rewrite in_cons; move => /orP; case => [/eqP ->|/B1A[mM]].
+  split => [m mM | m]; last by rewrite in_cons => - /orP; case=> [/eqP ->|/B1A[mM]].
   have [d dA dam] := mcM1 m mM; have mdwM1 : M1 (m - d * w).
     split; [have Mdwm := Mm d w m dA wM mM; have := Mm _ _ _ A0 Mdwm Mdwm |].
       by rewrite mul0r sub0r opprB.
@@ -525,17 +525,17 @@ have [X Xb] : exists X, basis_of_mod A (int_closure A L) X.
   apply/(Mbasis _ b2 _ b2f) => [| m [mL mI]]; first by apply/int_mod_closed.
   pose r : n.-tuple L0 := [tuple (coord b2 i m)%:A | i < n]; rewrite /span_mod size_tuple.
   exists r; have rci (i : 'I_n) : r`_i = (coord b2 i m)%:A by rewrite -tnth_nth tnth_mktuple.
-    apply/(all_nthP 0) => i; rewrite size_tuple; move => iB.
-    by have -> := rci (Ordinal iB); apply/b2H. 
-  move: mL; rewrite -b2s; move => /coord_span ->; apply/eq_bigr => i _.
+    apply/(all_nthP 0) => i; rewrite size_tuple => - iB.
+    by have -> := rci (Ordinal iB); apply/b2H.
+  move: mL; rewrite -b2s => - /coord_span ->; apply/eq_bigr => i _.
   by rewrite rci mulr_algl.
 exists X => //; move: Xb => [/eqP-Xf [Xs Xg]]; rewrite -Xf eqn_leq; apply/andP; split.
   by apply/dimvS/span_subvP => m /Xg[mL _].
 have /andP[/eqP-b1s _] := b1B; rewrite -b1s; apply/dimvS/span_subvP => b /tnthP-[i ->] {b}.
 rewrite (tnth_nth 0); have [r /all_tnthP-rA ->] : span_mod A X b1`_i.
   by apply/Xs; rewrite /int_closure (basis_mem b1B) ?mem_nth ?size_tuple => //.
-apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0); move => /Asub1/vlineP[c ->].
-by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth. 
+apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0) => - /Asub1/vlineP[c ->].
+by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth.
 Qed.
 
 End BasisLemma.
\ No newline at end of file
diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v
index d74288c..0a5b655 100644
--- a/mathcomp/attic/amodule.v
+++ b/mathcomp/attic/amodule.v
@@ -143,7 +143,7 @@ Definition eprodv vs ws := span (Tuple (size_eprodv vs ws)).
 Local Notation "A :* B" := (eprodv A B) : vspace_scope.
 
 Lemma memv_eprod vs ws a b : a \in vs -> b \in ws -> a :* b \in (vs :* ws)%VS.
-Proof. 
+Proof.
 move=> Ha Hb.
 rewrite (coord_vbasis Ha) (coord_vbasis Hb).
 rewrite linear_sum /=; apply: memv_suml => j _.
@@ -190,7 +190,7 @@ move=> vs; apply subv_anti; apply/andP; split.
   apply/eprodvP=> a b Ha; case/vlineP=> k1 ->.
   by rewrite linearZ /= rmul1 memvZ.
 apply/subvP=> v Hv.
-rewrite (coord_vbasis Hv); apply: memv_suml=> [] [i Hi] _ /=.  
+rewrite (coord_vbasis Hv); apply: memv_suml=> [] [i Hi] _ /=.
 apply: memvZ.
 rewrite -[_`_i]rmul1; apply: memv_eprod; last by apply: memv_line.
 by apply: vbasis_mem; apply: mem_nth; rewrite size_tuple.
@@ -211,9 +211,9 @@ Qed.
 Lemma eprodv_addl: left_distributive eprodv addv.
 Proof.
 move=> vs1 vs2 ws; apply subv_anti; apply/andP; split.
-  apply/eprodvP=> a b;case/memv_addP=> v1 Hv1 [v2 Hv2 ->] Hb.
+  apply/eprodvP=> a b; case/memv_addP=> v1 Hv1 [v2 Hv2 ->] Hb.
   by rewrite rmulD; apply: memv_add; apply: memv_eprod.
-apply/subvP=> v;  case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
+apply/subvP=> v; case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
 apply: memvD.
   by move: v1 Hv1; apply/subvP; apply: eprodvSl; apply: addvSl.
 by move: v2 Hv2; apply/subvP; apply: eprodvSl; apply: addvSr.
@@ -222,9 +222,9 @@ Qed.
 Lemma eprodv_sumr vs ws1 ws2 : (vs :* (ws1 + ws2) = vs :* ws1 + vs :* ws2)%VS.
 Proof.
 apply subv_anti; apply/andP; split.
-  apply/eprodvP=> a b Ha;case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
+  apply/eprodvP=> a b Ha; case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
   by rewrite linearD; apply: memv_add; apply: memv_eprod.
-apply/subvP=> v;  case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
+apply/subvP=> v; case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
 apply: memvD.
   by move: v1 Hv1; apply/subvP; apply: eprodvSr; apply: addvSl.
 by move: v2 Hv2; apply/subvP; apply: eprodvSr; apply: addvSr.
@@ -244,7 +244,7 @@ Proof. by move=> al; apply: subvf. Qed.
 
 Lemma memv_mod_mul : forall ms al m a, 
   modv ms al -> m \in ms -> a \in al -> m :* a \in ms.
-Proof. 
+Proof.
 move=> ms al m a Hmo Hm Ha; apply: subv_trans Hmo.
 by apply: memv_eprod.
 Qed.
@@ -262,7 +262,7 @@ Lemma modv_cap : forall ms1 ms2 al ,
 Proof.
 move=> ms1 ms2 al Hm1 Hm2.
 by rewrite /modv subv_cap; apply/andP; split;
-  [apply: subv_trans Hm1 | apply: subv_trans Hm2]; 
+  [apply: subv_trans Hm1 | apply: subv_trans Hm2];
    apply: eprodvSl; rewrite (capvSr,capvSl).
 Qed.
 
@@ -324,7 +324,7 @@ Lemma modf_add : forall f1 f2 ms al,
 Proof.
 move=> f1 f2 ms al Hm1 Hm2; apply/allP=> [] [v x].
 case/allpairsP=> [[x1 x2] [I1 I2 ->]]; rewrite !lfunE rmulD /=.
-move/modfP: Hm1->; try apply: vbasis_mem=>//.
+move/modfP: Hm1->; try apply: vbasis_mem=> //.
 by move/modfP: Hm2->; try apply: vbasis_mem.
 Qed.
 
@@ -414,7 +414,7 @@ rewrite memv_cap; apply/andP; split.
   apply: memvB=> //; apply: subv_trans Hsub.
   by rewrite -If; apply: memv_img; apply: memvf.
 rewrite memv_ker linearB /= (Himf (f v)) ?subrr // /in_mem /= -If.
-by apply: memv_img; apply: memvf. 
+by apply: memv_img; apply: memvf.
 Qed.
 
 End ModuleRepresentation.
diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v
index fefa0d2..a75a226 100644
--- a/mathcomp/attic/fib.v
+++ b/mathcomp/attic/fib.v
@@ -59,15 +59,15 @@ Proof. by []. Qed.
 Lemma lin_fib_alt : forall n a b,
   lin_fib a b n.+2 = lin_fib a b n.+1 + lin_fib a b n.
 Proof.
-case=>//; elim => [//|n IHn] a b.
+case=> //; elim=> [//|n IHn] a b.
 by rewrite lin_fibSS (IHn b (b + a)) lin_fibE.
 Qed.
 
 Lemma fib_is_linear : fib =1 lin_fib 0 1.
 Proof.
-move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn].
+move=> n; elim: n {-2}n (leqnn n)=> [n|n IHn].
   by rewrite leqn0; move/eqP=>->.
-case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite fibSS lin_fib_alt.
+case=> //; case=> // n0; rewrite ltnS=> ltn0n; rewrite fibSS lin_fib_alt.
 by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)).
 Qed.
 
@@ -132,7 +132,7 @@ case: m=> [|[|m]] Hm.
 - by rewrite eq_sym fib_eq1 orbF [1==_]eq_sym; case: eqP.
 have: 1 < m.+2 < n by [].
 move/fib_smonotone; rewrite ltn_neqAle; case/andP; move/negPf=> -> _.
-case: n Hm=> [|[|n]] //;rewrite ltn_neqAle; case/andP; move/negPf=> ->.
+case: n Hm=> [|[|n]] //; rewrite ltn_neqAle; case/andP; move/negPf=> ->.
 by rewrite andbF.
 Qed.
 
@@ -154,7 +154,7 @@ case/orP: (Hf _ (dvdn_fib _ _ (dvdn_mulr d (dvdnn k)))).
   rewrite fib_eq; case/or3P; first by move/eqP<-; rewrite eqxx orbT.
     by case/andP=>->.
   by rewrite Hk; case: (d)=> [|[|[|]]].
-rewrite fib_eq; case/or3P; last by case/andP;move/eqP->; case: (d)=> [|[|]].
+rewrite fib_eq; case/or3P; last by case/andP; move/eqP->; case: (d)=> [|[|]].
   rewrite -{1}[k]muln1; rewrite eqn_mul2l; case/orP; move/eqP=> HH.
     by move: Pp; rewrite Hp HH.
   by rewrite -HH eqxx.
@@ -216,9 +216,9 @@ Proof. by []. Qed.
 
 Lemma lucas_is_linear : lucas =1 lin_fib 2 1.
 Proof.
-move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn].
+move=> n; elim: n {-2}n (leqnn n)=> [n|n IHn].
   by rewrite leqn0; move/eqP=>->.
-case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt.
+case=> //; case=> // n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt.
 by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)).
 Qed.
 
@@ -329,7 +329,7 @@ Local Notation "''M{' l } " := (seq2matrix _ _ l).
 
 Lemma matrix_fib : forall n,
   'M{[:: [::(fib n.+2)%:R; (fib n.+1)%:R];
-         [::(fib n.+1)%:R;    (fib n)%:R]]} =  
+         [::(fib n.+1)%:R; (fib n)%:R]]} =  
  ('M{[:: [:: 1; 1];
          [:: 1; 0]]})^+n.+1 :> 'M[R]_(2,2).
 Proof.
diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v
index a1a987b..7098af9 100644
--- a/mathcomp/attic/forms.v
+++ b/mathcomp/attic/forms.v
@@ -20,7 +20,7 @@ Variable (R : fieldType).
 Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x .
 
 Lemma r2rv_morph_p : linear r2rv.
-Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j;rewrite !mxE. Qed.
+Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j; rewrite !mxE. Qed.
 
 Canonical Structure r2rv_morph := Linear r2rv_morph_p.
 
@@ -28,8 +28,8 @@ Definition rv2r (A: 'rV[R]_1): R^o := A 0 0.
 
 Lemma r2rv_bij : bijective r2rv.
 Proof.
-exists rv2r; first by move => x; rewrite /r2rv /rv2r /= mxE.
-by move => x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=.
+exists rv2r; first by move=> x; rewrite /r2rv /rv2r /= mxE.
+by move=> x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=.
 Qed.
 
 Canonical Structure  RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij.
@@ -48,7 +48,7 @@ Variable (F : fieldType) (V : vectType  F).
 Section SesquiLinearFormDef.
 
 Structure fautomorphism:= FautoMorph {fval :> F -> F;
-                                      _ : rmorphism  fval; 
+                                      _ : rmorphism  fval;
                                       _ : bijective fval}.
 Variable theta: fautomorphism.
 
@@ -72,7 +72,7 @@ Variable f : sesquilinear_form.
 Lemma bilin1 :  forall x, {morph f x : y z / y + z}. Proof. by case f. Qed.
 Lemma bilin2 :  forall x, {morph f ^~  x : y z / y + z}. Proof. by case f. Qed.
 Lemma bilina1 :  forall a x y, f (a *: x) y = a * f x y. Proof. by case f. Qed.
-Lemma bilina2 : forall a x y, f x (a *: y) = (theta  a) * (f x y). 
+Lemma bilina2 : forall a x y, f x (a *: y) = (theta  a) * (f x y).
 Proof. by case f. Qed.
 
 End SesquiLinearFormDef.
@@ -97,9 +97,9 @@ Inductive symmetricf (f : sqlf): Prop :=
 Lemma fsym_f0: forall  (f: sqlf) x y, (symmetricf f) ->  
                                         (f x y = 0  <-> f y x = 0).
 Proof.
-move => f x y ;case; first by  move=>  [Htheta Hf];split; rewrite Hf.
-  by move=>  [Htheta Hf];split; rewrite Hf; move/eqP;rewrite oppr_eq0; move/eqP->.
-move=> Htheta;split; first by rewrite (Htheta y x) => ->; rewrite rmorph0.
+move=> f x y; case; first by  move=> [Htheta Hf]; split; rewrite Hf.
+  by move=> [Htheta Hf]; split; rewrite Hf; move/eqP; rewrite oppr_eq0; move/eqP->.
+move=> Htheta; split; first by rewrite (Htheta y x) => ->; rewrite rmorph0.
 by rewrite (Htheta x y) => ->; rewrite rmorph0.
 Qed.
 
@@ -114,21 +114,21 @@ Section orthogonal.
 Definition orthogonal x y := f x y = 0.
 
 Lemma ortho_sym: forall x y, orthogonal x y <-> orthogonal y x.
-Proof. by move=> x y; apply:fsym_f0. Qed.
+Proof. by move=> x y; apply: fsym_f0. Qed.
 
 Theorem Pythagore: forall u v, orthogonal u v -> f (u+v) (u+v)  = f u u  + f v v.
 Proof.
-move => u v Huv; case:(ortho_sym  u v ) => Hvu _.
+move=> u v Huv; case: (ortho_sym  u v ) => Hvu _.
 by rewrite !bilin1 !bilin2 Huv (Hvu Huv) add0r addr0.
 Qed.
 
 Lemma orthoD : forall u v w , orthogonal u v -> orthogonal u w -> orthogonal u (v + w).
 Proof.
-by move => u v w Huv Huw; rewrite  /orthogonal bilin1 Huv Huw add0r.
+by move=> u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r.
 Qed.
 
 Lemma orthoZ: forall u v a, orthogonal u v ->  orthogonal (a *: u) v.
-Proof. by move => u v a Huv; rewrite  /orthogonal bilina1 Huv mulr0. Qed.
+Proof. by move=> u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed.
 
 Variable x:V.
 
@@ -139,7 +139,7 @@ Definition alpha_lfun := (lfun_of_fun alpha).
 Definition  xbar := lker alpha_lfun .
 
 Lemma alpha_lin: linear alpha.
-Proof. by move => a b c; rewrite /alpha bilin2 bilina1. Qed.
+Proof. by move=> a b c; rewrite /alpha bilin2 bilina1. Qed.
 
 
 
@@ -151,10 +151,10 @@ Qed.
 
 
 Lemma dim_xbar :forall vs,(\dim vs ) -  1 <= \dim (vs :&: xbar).
-Proof. 
+Proof.
 move=> vs; rewrite -(addKn 1 (\dim (vs :&: xbar))) addnC leq_sub2r //.
 have H :\dim  (alpha_lfun @: vs )<= 1 by rewrite -(dimR F) -dimvf dimvS // subvf.
-by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))). 
+by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))).
 Qed.
 
 (* to be improved*)
@@ -162,16 +162,16 @@ Lemma xbar_eqvs: forall vs,  (forall v , v \in vs -> orthogonal v x )-> \dim (vs
 move=> vs  Hvs.
 rewrite -(limg_ker_dim alpha_lfun vs).
 suff-> : \dim (alpha_lfun @: vs) = 0%nat by rewrite addn0.
-apply/eqP; rewrite dimv_eq0; apply /vspaceP => w.
-rewrite memv0;apply/memv_imgP.
+apply/eqP; rewrite dimv_eq0; apply/vspaceP => w.
+rewrite memv0; apply/memv_imgP.
 case e: (w==0).
-  exists 0; split ;first by rewrite mem0v.
+  exists 0; split; first by rewrite mem0v.
   apply sym_eq; rewrite (eqP e).
   rewrite (lfun_of_funK alpha_lin 0).
   rewrite /alpha_lfun /alpha /=.
-  by move:(bilina1 f 0 x x); rewrite scale0r mul0r.
-move/eqP:e =>H2;case=> x0 [Hx0 Hw].
-apply H2;rewrite Hw;move: (Hvs x0 Hx0).
+  by move: (bilina1 f 0 x x); rewrite scale0r mul0r.
+move/eqP:e =>H2; case=> x0 [Hx0 Hw].
+apply H2; rewrite Hw; move: (Hvs x0 Hx0).
 rewrite /orthogonal.
 by rewrite (lfun_of_funK alpha_lin x0).
 Qed.
@@ -189,9 +189,9 @@ Import GRing.Theory.
 
 Lemma f2Q:  forall x, Q x + Q x = f x x.
 Proof.
-move=> x; apply:(@addrI _ (Q x + Q x)).
+move=> x; apply: (@addrI _ (Q x + Q x)).
 rewrite !addrA  -quadQ -[x + x](scaler_nat 2) quadQ.
-by rewrite  -mulrA !mulr_natl -addrA.
+by rewrite -mulrA !mulr_natl -addrA.
 Qed.
 
 End LinearForm.
diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v
index 4902a47..16bbe1e 100644
--- a/mathcomp/attic/galgebra.v
+++ b/mathcomp/attic/galgebra.v
@@ -55,11 +55,11 @@ Definition mulrg v1 v2 :=
  GAlg ([ffun g => \sum_(k : gT) (v1 k) * (v2 ((k^-1) * g)%g)]).
 
 Lemma addrgA : associative addrg.
-Proof. 
+Proof.
 by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrA.
 Qed.
 Lemma addrgC : commutative addrg.
-Proof. 
+Proof.
 by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrC.
 Qed.
 Lemma addr0g : left_id g0 addrg.
diff --git a/mathcomp/attic/multinom.v b/mathcomp/attic/multinom.v
index 175da6c..96a8071 100644
--- a/mathcomp/attic/multinom.v
+++ b/mathcomp/attic/multinom.v
@@ -107,7 +107,7 @@ Definition multi_var n (i : 'I_n) := cast_multi (subnK (valP i)) 'X.
 Notation "'X_ i" := (multi_var i).
 
 Lemma inject_is_rmorphism : forall m n, rmorphism (@inject n m).
-Proof. 
+Proof.
 elim=> // m ihm n /=; have ->: inject m = RMorphism (ihm n) by [].
 by rewrite -/(_ \o _); apply: rmorphismP.
 Qed.
@@ -132,14 +132,14 @@ Lemma cast_multi_inj n i i' n' (m1 m2 : multi n)
   cast_multi p1 m1 == cast_multi p2 m2 = (m1 == m2).
 Proof.
 have := p2; rewrite -{1}[n']p1; move/eqP; rewrite eqn_add2r.
-move=> /eqP /= Eii; move:p2; rewrite Eii=> p2 {Eii}.
+move=> /eqP /= Eii; move: p2; rewrite Eii=> p2 {Eii}.
 have <-: p1 = p2; first exact: nat_irrelevance.
 apply/idP/idP; last by move/eqP->.
-move => Hm {p2}.
+move=> Hm {p2}.
 have : inject i m1 = inject i m2; last first.
    by move/eqP; rewrite (inj_eq (@inject_inj _ _)).
-move: Hm; move:(p1); rewrite -p1 => p2. 
-rewrite (_ : p2 = erefl (i+n)%N); last exact: nat_irrelevance. 
+move: Hm; move: (p1); rewrite -p1 => p2.
+rewrite (_ : p2 = erefl (i+n)%N); last exact: nat_irrelevance.
 by move/eqP.
 Qed.
 
@@ -195,8 +195,8 @@ Lemma interp_cast_multi n n' m (nltn' : n <= n') :
 Proof.
 move=> dmltn; have dmltn' := (leq_trans dmltn nltn').
 elim: m nltn' dmltn dmltn'.
-+ move=> a /= nltn' dmltn dmltn'. 
-  apply/eqP; rewrite /multiC. 
++ move=> a /= nltn' dmltn dmltn'.
+  apply/eqP; rewrite /multiC.
   by rewrite cast_multi_add /= cast_multi_inj.
 +  move=> N /= nltn' dmltn dmltn'.
   move: (refl_equal (_ N < n')) (refl_equal (_ N < n)).
diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v
index 332d841..b2025a7 100644
--- a/mathcomp/attic/tutorial.v
+++ b/mathcomp/attic/tutorial.v
@@ -59,7 +59,7 @@ Lemma andb_sym2 : forall A B : bool, A && B -> B && A.
 Proof. by case; case. Qed.
 
 Lemma andb_sym3 : forall A B : bool, A && B -> B && A.
-Proof. by do 2! case. Qed.
+Proof. by do 2!case. Qed.
 
 Variables (C D : Prop) (hC : C) (hD : D).
 Check (and C D).