running semi-automated linting on the whole library

10 files changed, 50 insertions, 50 deletions

diff --git a/mathcomp/real_closed/bigenough.v b/mathcomp/real_closed/bigenough.v
index 90e46e8..1ee8bef 100644
--- a/mathcomp/real_closed/bigenough.v
+++ b/mathcomp/real_closed/bigenough.v
@@ -28,7 +28,7 @@ Module BigEnough.
 
 Record big_rel_class_of T (leq : rel T) := 
   BigRelClass {
-      leq_big_internal_op : rel T; 
+      leq_big_internal_op : rel T;
       bigger_than_op : seq T -> T;
       _ : leq_big_internal_op = leq;
       _ : forall i s, leq_big_internal_op i (bigger_than_op (i :: s));
diff --git a/mathcomp/real_closed/cauchyreals.v b/mathcomp/real_closed/cauchyreals.v
index 9d2dff3..1d7d7ab 100644
--- a/mathcomp/real_closed/cauchyreals.v
+++ b/mathcomp/real_closed/cauchyreals.v
@@ -447,7 +447,7 @@ rewrite -{1}[x](addrNK z) -{1}[p.[x]](addrNK p.[z]).
 rewrite !addrA -![_ - _ + _ - _]addrA mulrDr ltr_add //.
   rewrite -ltr_pdivl_mulr ?subr_gt0 //.
   by rewrite ltr_minl hk1 ?gtr_eqF.
-rewrite  -ltr_pdivl_mulr ?subr_gt0 //.
+rewrite -ltr_pdivl_mulr ?subr_gt0 //.
 by rewrite ltr_minl hk2 ?orbT ?gtr_eqF.
 Qed.
 
@@ -1325,7 +1325,7 @@ have upx_eq0 : u.[x] * p.[x] == 0 by rewrite px0 mul_creal0.
 pose_big_enough i.
   have := (erefl ((1 : {poly F}).[x i])).
   rewrite -{1}hpq /= hornerD hornerC.
-  set upxi := (u * _).[_]; move=> hpqi.
+  set upxi := (u * _).[_] => - hpqi.
   apply: (@neq_crealP ((ubound v.[x])%CR^-1 / 2%:R) i i) => //.
     by rewrite pmulr_rgt0 ?gtr0E // ubound_gt0.
   rewrite /= subr0 ler_pdivr_mull ?ubound_gt0 //.
diff --git a/mathcomp/real_closed/complex.v b/mathcomp/real_closed/complex.v
index ef32266..30b4b04 100644
--- a/mathcomp/real_closed/complex.v
+++ b/mathcomp/real_closed/complex.v
@@ -58,7 +58,7 @@ Section ComplexEqChoice.
 
 Variable R : Type.
 
-Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [::a;  b].
+Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [::a; b].
 Definition complex_of_sqR (x : seq R) :=
   if x is [:: a; b] then Some (a +i* b) else None.
 
@@ -462,7 +462,7 @@ by rewrite -mulrA ['i%C * _]sqr_i mulrN1 opprB.
 Qed.
 
 Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0).
-Proof. 
+Proof.
 rewrite realE; simpc; rewrite [0 == _]eq_sym.
 by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb).
 Qed.
@@ -557,7 +557,7 @@ have F3: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) - a) / 2%:R.
 have F4: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) + a) / 2%:R.
   rewrite mulr_ge0 // -{2}[a]opprK subr_ge0 (ler_trans _ F2) //.
   by rewrite -(maxrN a) ler_maxr lerr orbT.
-congr (_ +i* _);  set u := if _ then _ else _.
+congr (_ +i* _); set u := if _ then _ else _.
   rewrite mulrCA !mulrA.
   have->: (u * u) = 1.
     rewrite /u; case: (altP (_ =P _)); rewrite ?mul1r //.
@@ -573,7 +573,7 @@ rewrite [_^+2 + _]addrC addrK -mulrA -expr2 sqrtrM ?exprn_even_ge0 //.
 rewrite !sqrtr_sqr -mulr_natr.
 rewrite [`|_^-1|]ger0_norm // -mulrA [_ * _%:R]mulrC divff //.
 rewrite mulr1 /u; case: (_ =P _)=>[->|].
-  by rewrite  normr0 mulr0.
+  by rewrite normr0 mulr0.
 by rewrite mulr_sg_norm.
 Qed.
 
@@ -998,7 +998,7 @@ Qed.
 
 Lemma Lemma3 K d : Eigen1Vec K d -> forall r, CommonEigenVec K d r.+1.
 Proof.
-move=> E1V_K_d; elim => [|r IHr m V]; first exact/Eigen1VecP.
+move=> E1V_K_d; elim=> [|r IHr m V]; first exact/Eigen1VecP.
 move: (\rank V) {-2}V (leqnn (\rank V)) => n {V}.
 elim: n m => [|n IHn] m V.
   by rewrite leqn0 => /eqP ->; rewrite dvdn0.
@@ -1111,7 +1111,7 @@ have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _).
   case: n {x} (vec_mx x) => [//|n] x in HrV u v *.
   do ?[rewrite -(scalemxAl, scalemxAr, scalerN, scalerDr)
       |rewrite (mulmxN, mulNmx, trmxK, trmx_mul)
-      |rewrite  ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=].
+      |rewrite ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=].
   congr (_ *: _).
   rewrite !(mulmxDr, mulmxDl, mulNmx, mulmxN, mulmxA, opprD, opprK).
   do ![move: (_ *m _ *m _)] => t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12.
diff --git a/mathcomp/real_closed/mxtens.v b/mathcomp/real_closed/mxtens.v
index 5189369..4e6b72a 100644
--- a/mathcomp/real_closed/mxtens.v
+++ b/mathcomp/real_closed/mxtens.v
@@ -186,7 +186,7 @@ rewrite !tensmxE castmxE /= cast_ord_id esymK !mxE /=.
 case: splitP=> i0' /= hi0'; case: splitP=> k /= hk.
 + case: (mxtens_indexP k) hk=> k0 k1 /=; rewrite tensmxE.
   move=> /(f_equal (edivn^~ p)); rewrite !edivn_eq // => [] [h0 h1].
-  by congr (r _ _ * N _ _); apply:val_inj; rewrite /= -?h0 ?h1.
+  by congr (r _ _ * N _ _); apply: val_inj; rewrite /= -?h0 ?h1.
 + move: hk (ltn_ord i1); rewrite hi0'.
   by rewrite [i0']ord1 mul0n mul1n add0n ltnNge=> ->; rewrite leq_addr.
 + move: (ltn_ord k); rewrite -hk hi0' ltnNge {1}mul1n.
@@ -194,7 +194,7 @@ case: splitP=> i0' /= hi0'; case: splitP=> k /= hk.
 case: (mxtens_indexP k) hk=> k0 k1 /=; rewrite tensmxE.
 rewrite hi0' mulnDl -addnA=> /addnI.
  move=> /(f_equal (edivn^~ p)); rewrite !edivn_eq // => [] [h0 h1].
-by congr (M _ _ * N _ _); apply:val_inj; rewrite /= -?h0 ?h1.
+by congr (M _ _ * N _ _); apply: val_inj; rewrite /= -?h0 ?h1.
 Qed.
 
 Lemma tens_row_mx {m n p q} (r : 'cV[R]_m) (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) :
diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v
index f5d0b38..4779540 100644
--- a/mathcomp/real_closed/ordered_qelim.v
+++ b/mathcomp/real_closed/ordered_qelim.v
@@ -189,7 +189,7 @@ Definition oclause_eq (T : eqType)(t1 t2 : oclause T) :=
 
 Lemma oclause_eqP (T : eqType) : Equality.axiom (@oclause_eq T).
 Proof.
-move=> t1 t2; apply: (iffP idP) => [|<-] /= ; last first.
+move=> t1 t2; apply: (iffP idP) => [|<-] /=; last first.
   by rewrite /oclause_eq; case: t1=> l1 l2 l3 l4; rewrite !eqxx.
 case: t1 => [l1 l2 l3 l4]; case: t2 => m1 m2 m3 m4 /=; case/and4P.
 by move/eqP=> -> /eqP -> /eqP -> /eqP ->.
@@ -780,11 +780,11 @@ Lemma odnf_to_oform_cat e c d : holds e (odnf_to_oform (c ++ d))
 Proof.
 elim: c d => [| tc c ihc] d /=; first by split => // hd; [right | case: hd].
 rewrite ihc /=; split.
-  case; first by case=> ?; case => ?; case => ? ?; left; left.
+  case; first by case=> ?; case=> ?; case=> ? ?; left; left.
   case; first by move=> ?; left; right.
   by move=> ?; right.
 case; last by move=> ?; right; right.
-case;  last by move=> ?; right; left.
+case; last by move=> ?; right; left.
 by do 3!case=> ?; move=> ?; left.
 Qed.
 
@@ -801,8 +801,8 @@ have -> : (holds e x1 /\ holds e x2 /\ holds e x3 /\ 0%:R <= eval e t /\
             holds e x4 \/ false) <->
           (0%:R <= eval e t) /\ (holds e x1 /\ holds e x2 /\ holds e x3 /\
             holds e x4 \/ false).
-  split; first by case=> //; do 4! (case => ?); move=> ?; split => //; left.
-  by case=> ?; case => //; do 3! (case=> ?); move=> ?; left.
+  split; first by case=> //; do 4!(case=> ?); move=> ?; split => //; left.
+  by case=> ?; case=> //; do 3!(case=> ?); move=> ?; left.
 rewrite h {h} /= !map_cat /= -!map_comp.
 set s1 := [seq _ | _ <- _]; set s2 := [seq _ | _ <- _].
 set s3 := [seq _ | _ <- _]. rewrite odnf_to_oform_cat.
@@ -822,7 +822,7 @@ rewrite /s2 /s1.
 elim: (leq_elim_aux eq_l lt_l le_l) => /= [| t1 l ih]; first by split=> // [[]].
 rewrite /= ih; split.
   case; last by case=> -> ?; split=> //; right.
-  by case; case=> /eqP ? ?; do 2! case=> ?; move=> _; split=>//; left.
+  by case; case=> /eqP ? ?; do 2!case=> ?; move=> _; split=> //; left.
 case=> /eqP ?; case; first by do 3!case=> ?; move=> _; left.
 by right; split=> //; apply/eqP.
 Qed.
@@ -857,7 +857,7 @@ rewrite -/f in ih; case/orP.
   move=> u. rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA.
   case/orP; first by move->; rewrite !orbT.
   rewrite !orbA [_ || (_ \in eq1)]orbC; move: (h u); rewrite !mem_cat=> hu.
-  by move/hu; do 2! (case/orP; last by move->; rewrite !orbT); move->.
+  by move/hu; do 2!(case/orP; last by move->; rewrite !orbT); move->.
 case/mapP=> y yin ye.
 move: (ih lt1 (f y)); rewrite mem_map //; last first.
   by move=> u v; rewrite /f /=; case.
@@ -865,7 +865,7 @@ move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h.
 move=> u; rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA.
 case/orP; first by move->; rewrite !orbT.
 rewrite !orbA [_ || (_ \in eq1)]orbC; move: (h u); rewrite !mem_cat=> hu.
-by move/hu; do 2! (case/orP; last by move->; rewrite !orbT); move->.
+by move/hu; do 2!(case/orP; last by move->; rewrite !orbT); move->.
 Qed.
 
 
@@ -885,9 +885,9 @@ have -> : holds e x1 /\
    false <->
           (eval e t <> 0%:R) /\ (holds e x1 /\ holds e x2 /\ holds e x3 /\
             holds e x4 \/ false).
-  split; case => //.
+  split; case=> //.
   - by case=> ?; case; case=> ? ? [] ? ?; split=> //; left.
-  - by move=> ?; case => //; do 3! case => ?; move=> ?; left.
+  - by move=> ?; case=> //; do 3!case=> ?; move=> ?; left.
 rewrite h {h} /= !map_cat /= -!map_comp.
 set s1 := [seq _ | _ <- _]; set s2 := [seq _ | _ <- _].
 set s3 := [seq _ | _ <- _]; rewrite odnf_to_oform_cat.
@@ -904,7 +904,7 @@ suff {x1 x2 x3 x4} /= -> :
   rewrite ih; split.
     case; first by case=> ?; case=> _; case; case=> -> ? ?; split=> //; left.
     by case=> ? ?; split=> //; right.
-  by case=> ->; case; [case=> ?; case=> _; case=> ? ?; left| move=> ? ; right].
+  by case=> ->; case; [case=> ?; case=> _; case=> ? ?; left| move=> ?; right].
 rewrite /s1 /s2.
 elim: (neq_elim_aux lt_l neq_l) => /= [| t1 l ih] /=; first by split => //; case.
 set y1 := foldr _ _ _; set y2 := foldr _ _ _; set y3 := foldr _ _ _.
@@ -922,7 +922,7 @@ Lemma terms_of_neq_leq_elim oc1 oc2:
   oc2 \in (oclause_neq_leq_elim oc1) ->
   {subset (terms_of_oclause oc2) <= (terms_of_oclause oc1) ++ map Opp oc1.2}.
 Proof.
-rewrite /oclause_neq_leq_elim /flatten; rewrite foldr_map.
+rewrite /oclause_neq_leq_elim/flatten; rewrite foldr_map.
 suff : forall oc3,
   oc3 \in (oclause_leq_elim oc1) ->
   (terms_of_oclause oc3 =i terms_of_oclause oc1) /\ oc3.2 = oc1.2.
@@ -938,7 +938,7 @@ rewrite map_cat mem_cat; move: ih.
 elim: (leq_elim_aux eq1 lt1 le1) => [| t2 l2 ih2] //=; rewrite !in_cons.
 move=> h1; case/orP=> /=.
   case/orP; first by case/eqP.
-  by move=> h2; apply: ih2; rewrite ?h2 //; move=> h3; apply: h1; rewrite h3 orbT.
+  by move=> h2; apply: ih2; rewrite ?h2 // => - h3; apply: h1; rewrite h3 orbT.
 case/orP; first by case/eqP.
 move=> h3; apply: ih2; last by rewrite h3 orbT.
 by move=> h2; apply: h1; rewrite h2 orbT.
@@ -1009,7 +1009,7 @@ rewrite -[holds e (_ \/ _)]/(holds e _ \/ holds e _).
 suff <- : (oclause_neq_elim t1) = map w_to_oclause
            [seq (let: Oclause eq_l _  lt_l _ := x in (eq_l, lt_l))
               | x <- oclause_neq_elim t1].
-  by rewrite ih1 //; move=> oc hoc; apply: h4; rewrite in_cons hoc orbT.
+  by rewrite ih1 // => - oc hoc; apply: h4; rewrite in_cons hoc orbT.
 have : forall oc, oc \in (oclause_neq_elim t1) -> oc.2 = [::] /\ oc.4 = [::].
   move=> oc hoc; move/oclause_neq_elim2: (hoc); case/andP=> /eqP -> /eqP ->.
   by move/eqP: (h4 _ (mem_head _ _))->.
diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v
index f84abb6..4a96dcc 100644
--- a/mathcomp/real_closed/polyorder.v
+++ b/mathcomp/real_closed/polyorder.v
@@ -139,9 +139,9 @@ Qed.
 Lemma mu_mul p q x : p * q != 0 ->
   \mu_x (p * q) = (\mu_x p + \mu_x q)%N.
 Proof.
-move=>hpqn0; apply/eqP; rewrite eq_sym -muP//.
+move=> hpqn0; apply/eqP; rewrite eq_sym -muP//.
 rewrite exprD dvdp_mul ?root_mu//=.
-move:hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0.
+move: hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0.
 move: (mu_spec x hp0)=> [qp qp0 hp].
 move: (mu_spec x hq0)=> [qq qq0 hq].
 rewrite {2}hp {2}hq exprS exprD !mulrA [qp * _ * _]mulrAC.
diff --git a/mathcomp/real_closed/polyrcf.v b/mathcomp/real_closed/polyrcf.v
index 9e73204..8aaeb97 100644
--- a/mathcomp/real_closed/polyrcf.v
+++ b/mathcomp/real_closed/polyrcf.v
@@ -441,7 +441,7 @@ elim: (size p) a b lab pa0 pb0=> [|n ihn] a b lab pa0 pb0 max_roots.
   rewrite (@max_roots [::]) //=.
   by exists (mid a b); rewrite ?mid_in_itv // derivE horner0.
 case: (@rolle_weak a b p); rewrite // ?pa0 ?pb0 //=.
-move=> c hc;  case: (altP (_ =P 0))=> //= p'c0 pc0; first by exists c.
+move=> c hc; case: (altP (_ =P 0))=> //= p'c0 pc0; first by exists c.
 suff: { d : R | d \in `]a, c[ & (p^`()).[d] = 0 }.
   case=> [d hd] p'd0; exists d=> //.
   by apply: subitvPr hd; rewrite //= (itvP hc).
@@ -860,7 +860,7 @@ rewrite in_cons; case ezy: (z == y)=> /=.
   by rewrite (eqP ezy) py0 andbT (subitvPr _ hy) //= ?(itvP hx).
 rewrite -(ihs y) //; last exact: path_sorted ss; last first.
   by rewrite inE /= (itvP hx) (itvP hy).
-case pz0: root;  rewrite ?(andbT, andbF) //.
+case pz0: root; rewrite ?(andbT, andbF) //.
 rewrite (@itv_splitU2 _ y); last by rewrite (subitvPr _ hy) //= (itvP hx).
 rewrite ezy /=; case: (z \in `]y, b[); rewrite ?orbF ?orbT //.
 by apply/negP=> hz; move: (hay z); rewrite hz pz0 in_nil.
@@ -913,7 +913,7 @@ move: (roots_on_nil har1).
 case pr1 : (root p r1); case/monotonic_rootN => hrootsl; last 2 first.
 - exists s; constructor=> //.
   by rewrite -[s]cat0s; apply: (cat_roots_on hr1)=> //; rewrite pr1.
-- case:hrootsl=> r hr; exists (r::s); constructor=> //=.
+- case: hrootsl=> r hr; exists (r::s); constructor=> //=.
     by rewrite -cat1s; apply: (cat_roots_on hr1)=> //; rewrite pr1.
   rewrite path_min_sorted // => y; rewrite -hroot; case/andP=> hy _.
   rewrite (@ltr_trans _ r1) ?(itvP hy) //.
@@ -954,7 +954,7 @@ Proof. by case: rootsP=> //=; rewrite eqxx. Qed.
 
 Lemma roots_on_roots : forall p a b, p != 0 ->
   roots_on p `]a, b[ (roots p a b).
-Proof. by move=> a b p; case:rootsP. Qed.
+Proof. by move=> a b p; case: rootsP. Qed.
 Hint Resolve roots_on_roots.
 
 Lemma sorted_roots a b p : sorted <%R (roots p a b).
@@ -1012,7 +1012,7 @@ elim: s1 p a b s2 => [| r1 s1 ih] p a b [| r2 s2] ps1 ps2 rs1 rs2 //.
     move/(@sym_eq _ true); case/orP => hr2; first by rewrite (eqP hr2).
     move: ps1=> /=; move/(order_path_min (@ltr_trans R)); move/allP.
     move/(_ r2 hr2) => h1.
-    move: (rs2 r1);  rewrite (roots_on_root rs1) ?mem_head //.
+    move: (rs2 r1); rewrite (roots_on_root rs1) ?mem_head //.
     rewrite !(roots_on_in rs1) ?mem_head //= in_cons.
     move/(@sym_eq _ true); case/orP => hr1; first by rewrite (eqP hr1).
     move: ps2=> /=; move/(order_path_min (@ltr_trans R)); move/allP.
@@ -1212,7 +1212,7 @@ case; first by move->; rewrite /next_root eqxx.
   move=> c p0 ->; case: maxrP=> hab; last by rewrite itv_gte //= ltrW.
   by move=> hpz _ py0 hy; move/hpz:hy; rewrite rootE py0 eqxx.
 case: next_rootP => //; first by move->; rewrite eqxx.
-  by move=> y np0 py0 hy _ c _ _;  move/(_ _ hy); rewrite rootE py0 eqxx.
+  by move=> y np0 py0 hy _ c _ _; move/(_ _ hy); rewrite rootE py0 eqxx.
 by move=> c _ -> _ c' _ ->.
 Qed.
 
@@ -1507,11 +1507,11 @@ Lemma sgr_neighpr b p x :
 Proof.
 elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
   rewrite leqn0 size_poly_eq0 /neighpr; move/eqP=> -> /=.
-  by move=>y; rewrite next_root0 itv_xx.
+  by move=> y; rewrite next_root0 itv_xx.
 rewrite leq_eqVlt ltnS; case/orP; last exact: ihn.
 move/eqP=> sp; rewrite /sgp_right sp /=.
 case px0: root=> /=; last first.
-  move=> y; rewrite/neighpr => hy /=; symmetry.
+  move=> y; rewrite /neighpr => hy /=; symmetry.
   apply: (@polyrN0_itv `[x, y]); do ?by rewrite bound_in_itv /= (itvP hy).
   move=> z; rewrite (@itv_splitU _ x true) ?bound_in_itv /= ?(itvP hy) //.
   rewrite itv_xx /=; case/predU1P=> hz; first by rewrite hz px0.
@@ -1547,11 +1547,11 @@ Lemma sgr_neighpl a p x :
 Proof.
 elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {p} p.
   rewrite leqn0 size_poly_eq0 /neighpl; move/eqP=> -> /=.
-  by move=>y; rewrite prev_root0 itv_xx.
+  by move=> y; rewrite prev_root0 itv_xx.
 rewrite leq_eqVlt ltnS; case/orP; last exact: ihn.
 move/eqP=> sp; rewrite /sgp_right sp /=.
 case px0: root=> /=; last first.
-  move=> y; rewrite/neighpl => hy /=; symmetry.
+  move=> y; rewrite /neighpl => hy /=; symmetry.
   move: (negbT px0); rewrite -mu_gt0; last first.
     by apply: contraFN px0; move/eqP->; rewrite rootC.
   rewrite -leqNgt leqn0; move/eqP=> -> /=; rewrite expr0 mul1r.
diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v
index e1b3b97..272c44a 100644
--- a/mathcomp/real_closed/qe_rcf.v
+++ b/mathcomp/real_closed/qe_rcf.v
@@ -160,7 +160,7 @@ Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
   end.
 
 Lemma evalE (e : seq R) (t : term R) : eval e t = GRing.eval e t.
-Proof. by elim: t=> /=; do ?[move->|move=>?]. Qed.
+Proof. by elim: t=> /=; do ?[move->|move=> ?]. Qed.
 
 Definition qf_eval e := fix loop (f : formula R) : bool :=
   match f with
@@ -175,7 +175,7 @@ Definition qf_eval e := fix loop (f : formula R) : bool :=
   end%qfT.
 
 Lemma qf_evalE (e : seq R) (f : formula R) : qf_eval e f = ord.qf_eval e f.
-Proof. by elim: f=> /=; do ?[rewrite evalE|move->|move=>?]. Qed.
+Proof. by elim: f=> /=; do ?[rewrite evalE|move->|move=> ?]. Qed.
 
 Lemma to_rtermE (t : GRing.term R) :
   GRing.rterm t -> to_rterm t = t :> GRing.term _.
@@ -206,10 +206,10 @@ Lemma qf_formF (f : fF) : qf_form f.
 Proof. by elim: f=> // *; apply/andP; split. Qed.
 
 Lemma rtermF (t : tF) : GRing.rterm t.
-Proof. by elim: t=> //=; do ?[move->|move=>?]. Qed.
+Proof. by elim: t=> //=; do ?[move->|move=> ?]. Qed.
 
 Lemma rformulaF (f : fF) : rformula f.
-Proof. by elim: f=> /=; do ?[rewrite rtermF|move->|move=>?]. Qed.
+Proof. by elim: f=> /=; do ?[rewrite rtermF|move->|move=> ?]. Qed.
 
 Section If.
 
@@ -846,7 +846,7 @@ symmetry; rewrite /ctmat1.
 apply/matrixP => i j; rewrite !(big_ord_recl, big_ord0, mxE) /=.
 have halfP (K : numFieldType) : 2%:R^-1 + 2%:R^-1 = 1 :> K.
   by rewrite -mulr2n -[_ *+ 2]mulr_natl mulfV // pnatr_eq0.
-move: i; do ?[case => //=]; move: j; do ?[case => //=] => _ _;
+move: i; do ?[case=> //=]; move: j; do ?[case=> //=] => _ _;
 rewrite !(mulr1, mul1r, mulrN1, mulN1r, mulr0, mul0r, opprK);
 by rewrite !(addr0, add0r, oppr0, subrr, addrA, halfP).
 Qed.
diff --git a/mathcomp/real_closed/qe_rcf_th.v b/mathcomp/real_closed/qe_rcf_th.v
index 3aebce4..b125997 100644
--- a/mathcomp/real_closed/qe_rcf_th.v
+++ b/mathcomp/real_closed/qe_rcf_th.v
@@ -143,7 +143,7 @@ move/eqP: (rdivp_eq q p).
 rewrite eq_sym (can2_eq (addKr _ ) (addNKr _)); move/eqP=> hr.
 rewrite hr; case qpq0: (rdivp p q == 0).
   by rewrite (eqP qpq0) mul0r oppr0 add0r mu_mulC // lcn_neq0.
-rewrite  (leq_trans _ (mu_add _ _)) // -?hr //.
+rewrite (leq_trans _ (mu_add _ _)) // -?hr //.
 rewrite leq_min mu_opp mu_mul ?mulf_neq0 ?qpq0 ?q0 // leq_addl.
 by rewrite mu_mulC // lcn_neq0.
 Qed.
@@ -185,7 +185,7 @@ Definition ctmat n := (ctmat1 ^t n).
 Lemma ctmat_unit : forall n, zmxR (ctmat n) \in unitmx.
 Proof.
 case=> [|n] /=; first by rewrite map_mx1 ?unitmx1//; apply: zinjR_morph.
-elim:n=> [|n ihn] /=; first by  apply: ctmat1_unit.
+elim: n=> [|n ihn] /=; first by  apply: ctmat1_unit.
 rewrite map_mxT //.
 apply: tensmx_unit=> //; last exact: ctmat1_unit.
 by elim: n {ihn}=> // n ihn; rewrite muln_eq0.
@@ -277,7 +277,7 @@ Qed.
 
 Fixpoint sg_tab n : seq (seq int) :=
   if n is m.+1
-    then flatten (map (fun x => map (fun l => x :: l) (sg_tab m)) [::1;-1;0])
+    then flatten (map (fun x => map (fun l => x :: l) (sg_tab m)) [::1; -1; 0])
     else [::[::]].
 
 Lemma sg_tab_nil n : (sg_tab n == [::]) = false.
@@ -522,7 +522,7 @@ have [p'0|p'_neq0] := eqVneq p^`() 0.
   move/(root_size_gt1 p_neq0): rpx.
   by rewrite -subn_gt0 subn1 -size_deriv p'0 size_poly0.
 have p'q0: p^`() * q != 0 by rewrite mulf_neq0.
-move:(p'q0); rewrite mulf_eq0 negb_or; case/andP=> p'0 q0.
+move: (p'q0); rewrite mulf_eq0 negb_or; case/andP=> p'0 q0.
 have p0: p != 0 by move: p'0; apply: contra; move/eqP->; rewrite derivC.
 rewrite /jump  mu_mul// {1}(@mu_deriv_root _ _ p)// addn1 p'q0 /=.
 case emq: (\mu_(_) q)=> [|m].
@@ -825,10 +825,10 @@ wlog cpq: p q hpqa hpqb / coprimep p q => [hwlog|].
   apply: hwlog; rewrite ?coprimep_div_gcd ?p0 // rootM.
   + apply: contra hpqa; rewrite -!dvdp_XsubCl => /orP.
     case=> /dvdp_trans-> //; rewrite (dvdp_trans (divp_dvd _));
-    by rewrite  ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr).
+    by rewrite ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr).
   + apply: contra hpqb; rewrite -!dvdp_XsubCl => /orP.
     case=> /dvdp_trans-> //; rewrite (dvdp_trans (divp_dvd _));
-    by rewrite  ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr).
+    by rewrite ?(dvdp_gcdl, dvdp_gcdr) ?(dvdp_mulIl, dvdp_mulIr).
 have p0: p != 0 by apply: contraNneq hpqa => ->; rewrite mul0r rootC.
 have q0: q != 0 by apply: contraNneq hpqa => ->; rewrite mulr0 rootC.
 have pq0 : p * q != 0 by rewrite mulf_neq0.
@@ -903,7 +903,7 @@ pose m p q := maxn (size p) (size q).+1; rewrite -!/(m _ _).
 suff {p q} Hnext p q : q != 0 -> (m q (next_mod p q) < m p q)%N; last first.
   rewrite /m -maxnSS leq_max !geq_max !ltnS leqnn /= /next_mod.
   rewrite size_scale ?oppr_eq0 ?lcn_neq0 //=.
-  by move=> q_neq0; rewrite  ltn_rmodp ?q_neq0 ?orbT.
+  by move=> q_neq0; rewrite ltn_rmodp ?q_neq0 ?orbT.
 suff {p q} m_gt0 p q : (0 < m p q)%N; last by rewrite leq_max orbT.
 rewrite -[m p q]prednK //=; have [//|p_neq0] := altP (p =P 0).
 have [->|q_neq0] := altP (q =P 0); first by rewrite !aux0.
diff --git a/mathcomp/real_closed/realalg.v b/mathcomp/real_closed/realalg.v
index 69fb9c4..0cbba9f 100644
--- a/mathcomp/real_closed/realalg.v
+++ b/mathcomp/real_closed/realalg.v
@@ -229,7 +229,7 @@ Lemma root_inv_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
 Proof.
 rewrite /div_algcreal; case: eq_algcreal_dec=> [/(_ x_neq0)|x_neq0'] //=.
 case: simplify_algcreal=> x' px'0_neq0 [x'_neq0 eq_xx'].
-apply: is_root_annul_creal;rewrite /= -(@eq_creal_inv _ _ _ x_neq0) //.
+apply: is_root_annul_creal; rewrite /= -(@eq_creal_inv _ _ _ x_neq0) //.
 by apply: eq_crealP; exists m0=> * /=; rewrite div1r subrr normr0.
 Qed.