running semi-automated linting on the whole library

13 files changed, 51 insertions, 51 deletions

diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v
index b8ae7d6..e43f0f7 100644
--- a/mathcomp/ssrtest/absevarprop.v
+++ b/mathcomp/ssrtest/absevarprop.v
@@ -23,10 +23,10 @@ Variable Q1 : forall P1, Q 1 P1.
 
 Lemma testmE1 : myEx.
 Proof.
-apply: ExI 1 _ _ _ _. 
+apply: ExI 1 _ _ _ _.
   match goal with |- P 1 => exact: P1 | _ => fail end.
   match goal with |- P (1+1) => exact: P11 | _ => fail end.
-  match goal with |- forall p : P 1, Q 1 p => move=>*; exact: Q1 | _ => fail end.
+  match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end.
 match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end.
 Qed.
 
@@ -54,7 +54,7 @@ Hint Resolve P1.
 
 Lemma testmE12 : myEx.
 Proof.
-apply: ExI 1 _ _ _ _. 
+apply: ExI 1 _ _ _ _.
   match goal with |- P (1+1) => exact: P11 | _ => fail end.
   match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
 match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end.
@@ -68,7 +68,7 @@ Ltac ssrautoprop := trivial with SSR.
 
 Lemma testmE13 : myEx.
 Proof.
-apply: ExI 1 _ _ _ _. 
+apply: ExI 1 _ _ _ _.
   match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
 match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end.
 Qed.
@@ -84,7 +84,7 @@ Hint Resolve (Q1 P1) : SSR.
    thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *)
 Lemma testmE14 : myEx1.
 Proof.
-apply: ExI1 1 _ _ _ _.  
+apply: ExI1 1 _ _ _ _.
 match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end.
 Qed.
 
diff --git a/mathcomp/ssrtest/derive_inversion.v b/mathcomp/ssrtest/derive_inversion.v
index 71257d8..0a344b8 100644
--- a/mathcomp/ssrtest/derive_inversion.v
+++ b/mathcomp/ssrtest/derive_inversion.v
@@ -15,5 +15,5 @@ Set Implicit Arguments.
     | false => o = None
     end.
   Proof.
-  by case: b; elim/wf_inv=>//;case: o=>// a *; exists a.
+  by case: b; elim/wf_inv=> //; case: o=> // a *; exists a.
   Qed.
diff --git a/mathcomp/ssrtest/elim.v b/mathcomp/ssrtest/elim.v
index 9f0f139..0a7b777 100644
--- a/mathcomp/ssrtest/elim.v
+++ b/mathcomp/ssrtest/elim.v
@@ -7,7 +7,7 @@ Axiom daemon : False. Ltac myadmit := case: daemon.
 
 (* Ltac debugging feature: recursive elim + eq generation *)
 Lemma testL1 : forall A (s : seq A), s = s.
-Proof. 
+Proof.
 move=> A s; elim branch: s => [|x xs _].
 match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
 match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
@@ -15,7 +15,7 @@ Qed.
 
 (* The same but with explicit eliminator and a conflict in the intro pattern *)
 Lemma testL2 : forall A (s : seq A), s = s.
-Proof. 
+Proof.
 move=> A s; elim/last_ind branch: s => [|x s _].
 match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
 match goal with _ : _ =  rcons _ _ |- rcons _ _ = rcons _ _ => move: branch => // | _ => fail end.
@@ -23,17 +23,17 @@ Qed.
 
 (* The same but without names for variables involved in the generated eq *)
 Lemma testL3 : forall A (s : seq A), s = s.
-Proof. 
+Proof.
 move=> A s; elim branch: s; move: (s) => _.
 match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
-move=> _;match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
 Qed.
 
 Inductive foo : Type := K1 : foo | K2 : foo -> foo -> foo | K3 : (nat -> foo) -> foo.
 
 (* The same but with more intros to be done *)
 Lemma testL4 : forall (o : foo), o = o.
-Proof. 
+Proof.
 move=> o; elim branch: o.
 match goal with _ : _ = K1 |- K1 = K1 => move: branch => // | _ => fail end.
 move=> _; match goal with _ : _ = K2 _ _ |- K2 _ _ = K2 _ _ => move: branch => // | _ => fail end.
@@ -88,21 +88,21 @@ Qed.
 
 (* Patterns *)
 Lemma testP1: forall (x y : nat), (y == x) && (y == x) -> y == x.
-move=> x y; elim: {2}(_ == _) / eqP. 
-match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=>-> // | _ => fail end.
-match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=>_; rewrite andbC // | _ => fail end.
+move=> x y; elim: {2}(_ == _) / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
 Qed.
 
 (* The same but with an implicit pattern *)
 Lemma testP2 : forall (x y : nat), (y == x) && (y == x) -> y == x.
-move=> x y; elim: {2}_ / eqP. 
-match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=>-> // | _ => fail end.
-match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=>_; rewrite andbC // | _ => fail end.
+move=> x y; elim: {2}_ / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
 Qed.
 
 (* The same but with an eq generation switch *)
 Lemma testP3 : forall (x y : nat), (y == x) && (y == x) -> y == x.
-move=> x y; elim E: {2}_ / eqP. 
+move=> x y; elim E: {2}_ / eqP.
 match goal with _ : y = x |- (is_true ((y == x) && true) -> is_true (y == x)) => rewrite E; reflexivity | _ => fail end.
 match goal with _ : y <> x |- (is_true ((y == x) && false) -> is_true (y == x)) => rewrite E => /= H; exact H  | _ => fail end.
 Qed.
@@ -113,25 +113,25 @@ Lemma specP : spec 0 2 4. Proof. by constructor. Qed.
 
 Lemma testP4 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
 Proof.
-case: specP => a b c defa defb defc. 
+case: specP => a b c defa defb defc.
 match goal with |- (a.+1 + a.+1) * c = b + (a.+1 + a.+1) + (b + b) => subst; done | _ => fail end.
 Qed.
 
 Lemma testP5 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
 Proof.
-case: (1 + 1) _ / specP => a b c defa defb defc. 
+case: (1 + 1) _ / specP => a b c defa defb defc.
 match goal with |- b * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
 Qed.
 
 Lemma testP6 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
 Proof.
-case: {2}(1 + 1) _ / specP => a b c defa defb defc. 
+case: {2}(1 + 1) _ / specP => a b c defa defb defc.
 match goal with |- (a.+1 + a.+1) * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
 Qed.
 
 Lemma testP7 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
 Proof.
-case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc. 
+case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc.
 match goal with |- b * a.+4 = c + c => subst; done | _ => fail end.
 Qed.
 
@@ -276,7 +276,7 @@ Definition plus_ind := plus_rect.
 Lemma exF x y z: plus (plus x y) z = plus x (plus y z).
 elim/plus_ind: z / (plus _ z).
 match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
-Undo 2. 
+Undo 2.
 elim/plus_ind: (plus _ z).
 match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
 Undo 2.
diff --git a/mathcomp/ssrtest/have_transp.v b/mathcomp/ssrtest/have_transp.v
index fec720c..713f176 100644
--- a/mathcomp/ssrtest/have_transp.v
+++ b/mathcomp/ssrtest/have_transp.v
@@ -10,7 +10,7 @@ Proof.
 have [:s1] @h m : 'I_(n+m).+1.
   apply: Sub 0 _.
   abstract: s1 m.
-  by auto. 
+  by auto.
 cut (forall m, 0 < (n+m).+1); last assumption.
 rewrite [_ 1 _]/= in s1 h *.
 by [].
diff --git a/mathcomp/ssrtest/havesuff.v b/mathcomp/ssrtest/havesuff.v
index f97f445..4b0193a 100644
--- a/mathcomp/ssrtest/havesuff.v
+++ b/mathcomp/ssrtest/havesuff.v
@@ -9,7 +9,7 @@ Lemma test1 : (P -> G) -> P -> G.
 Proof.
 move=> pg p.
 have suff {pg} H : P.
-  match goal with |- P -> G => move=> _; exact: pg p | _ => fail end. 
+  match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
 match goal with H : P -> G |- G => exact: H p | _ => fail end.
 Qed.
 
@@ -17,7 +17,7 @@ Lemma test2 : (P -> G) -> P -> G.
 Proof.
 move=> pg p.
 have suffices {pg} H : P.
-  match goal with |- P -> G => move=> _;exact: pg p | _ => fail end. 
+  match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
 match goal with H : P -> G |- G => exact: H p | _ => fail end.
 Qed.
 
@@ -25,7 +25,7 @@ Lemma test3 : (P -> G) -> P -> G.
 Proof.
 move=> pg p.
 suff have {pg} H : P.
-  match goal with H : P |- G => exact: pg H | _ => fail end. 
+  match goal with H : P |- G => exact: pg H | _ => fail end.
 match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
 Qed.
 
@@ -33,7 +33,7 @@ Lemma test4 : (P -> G) -> P -> G.
 Proof.
 move=> pg p.
 suffices have {pg} H: P.
-  match goal with H : P |- G => exact: pg H | _ => fail end. 
+  match goal with H : P |- G => exact: pg H | _ => fail end.
 match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
 Qed.
 
diff --git a/mathcomp/ssrtest/intro_beta.v b/mathcomp/ssrtest/intro_beta.v
index 6b1b96d..4402be9 100644
--- a/mathcomp/ssrtest/intro_beta.v
+++ b/mathcomp/ssrtest/intro_beta.v
@@ -10,6 +10,6 @@ Definition C (P : T -> Prop) := forall x, P x.
 Axiom P : T -> T -> Prop.
 
 Lemma foo : C (fun x => forall y, let z := x in P y x).
-move=> a b. 
+move=> a b.
 match goal with |- (let y := _ in _) => idtac end.
 Admitted.
diff --git a/mathcomp/ssrtest/ltac_in.v b/mathcomp/ssrtest/ltac_in.v
index 06d8dc7..cec244d 100644
--- a/mathcomp/ssrtest/ltac_in.v
+++ b/mathcomp/ssrtest/ltac_in.v
@@ -10,9 +10,9 @@ Import Prenex Implicits.
 
 (* error 1 *)
 
-Ltac subst1 H := move: H ; rewrite {1} addnC; move => H.
+Ltac subst1 H := move: H; rewrite {1} addnC; move => H.
 Ltac subst2 H := rewrite addnC in H.
 
 Goal ( forall a b: nat, b+a = 0 -> b+a=0).
-Proof. move => a b hyp. subst1 hyp. subst2 hyp. done. Qed.
+Proof. move=> a b hyp. subst1 hyp. subst2 hyp. done. Qed.
 
diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v
index 95c3c00..22ca265 100644
--- a/mathcomp/ssrtest/rewpatterns.v
+++ b/mathcomp/ssrtest/rewpatterns.v
@@ -10,7 +10,7 @@ by move=> x y f; rewrite [_.+1](addnC x.+1).
 Qed.
 
 Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y).
-by move=> x y f; rewrite {2}[in f _]addnC. 
+by move=> x y f; rewrite {2}[in f _]addnC.
 Qed.
 
 Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)).
@@ -27,7 +27,7 @@ by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK *
 Qed.
 
 Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x).
-by move=> x y f; rewrite [in X in (f _ X)](addnC y). 
+by move=> x y f; rewrite [in X in (f _ X)](addnC y).
 Qed.
 
 Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x = 
@@ -37,7 +37,7 @@ Qed.
 
 Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x = 
                                        x + f (x + y) x + f (y + y) x.
-by move=> x y f E; rewrite {2}[in X in (f X _)]E. 
+by move=> x y f E; rewrite {2}[in X in (f X _)]E.
 Qed.
 
 Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x = 
@@ -52,22 +52,22 @@ Qed.
 
 Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x = 
                                      x + f (x + y) x + f (y + x) x.
-by move=> x y f E; rewrite {1}[X in (f X _)]addnC. 
+by move=> x y f E; rewrite {1}[X in (f X _)]addnC.
 Qed.
 
 Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = 
                                         x + f (x + y) x + f (y + y) (x + y).
-by move=> x y f E; rewrite {1}[in X in (f X X)]E. 
+by move=> x y f E; rewrite {1}[in X in (f X X)]E.
 Qed.
 
 Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = 
                                          x + f (x + y) x + f (y + y) (y + y).
-by move=> x y f E; rewrite [in X in (f X X)]E. 
+by move=> x y f E; rewrite [in X in (f X X)]E.
 Qed.
 
 Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) = 
                                          x + f (x + y) x + f (y + y) (y + y).
-by move=> x y f E; rewrite -[X in (f X X)]E. 
+by move=> x y f E; rewrite -[X in (f X X)]E.
 Qed.
 
 Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x).
diff --git a/mathcomp/ssrtest/set_pattern.v b/mathcomp/ssrtest/set_pattern.v
index 25b6967..5d22ef2 100644
--- a/mathcomp/ssrtest/set_pattern.v
+++ b/mathcomp/ssrtest/set_pattern.v
@@ -7,7 +7,7 @@ Axiom daemon : False. Ltac myadmit := case: daemon.
 Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end.
 Ltac T2 x := first [set t := (x in RHS)].
 Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac].
-Ltac T4 x := set t := (x in RHS);idtac.
+Ltac T4 x := set t := (x in RHS); idtac.
 Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end.
 
 From mathcomp
@@ -17,14 +17,14 @@ Lemma foo x y : x.+1 = y + x.+1.
 set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
 set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
 set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end.
-set t := (x in X in _ = X). 
+set t := (x in X in _ = X).
   match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
 set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
-set t := (y + (1 + x) as X in _ = X). 
+set t := (y + (1 + x) as X in _ = X).
   match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end.
 set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end.
 set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end.
-set t := ((x).+1 in X in _ = X). 
+set t := ((x).+1 in X in _ = X).
   match goal with |- x.+1 = y + t => rewrite /t {t} end.
 set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
 T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
@@ -32,7 +32,7 @@ T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
 T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
 T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
 T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
-rewrite [RHS]addnC. 
+rewrite [RHS]addnC.
   match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end.
 rewrite -[in RHS](@subnK 1 x.+1) //.
   match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end.
@@ -44,7 +44,7 @@ set t := (_.+1 in X in _ + X) in H |- *.
 set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end.
 set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end.
 set t : nat := 0. clear t.
-set t : nat := (x in RHS). 
+set t : nat := (x in RHS).
   match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
 set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end.
 (* set t := 0 + _. *)
diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v
index 9116ba2..3fc202f 100644
--- a/mathcomp/ssrtest/ssrsyntax1.v
+++ b/mathcomp/ssrtest/ssrsyntax1.v
@@ -14,7 +14,7 @@ Import ssreflect.
 
 Goal (forall a b, a + b = b + a).
 intros.
-rewrite 2![_ + _]plus_comm. 
+rewrite 2![_ + _]plus_comm.
 split.
 Abort.
 End Foo.
diff --git a/mathcomp/ssrtest/tc.v b/mathcomp/ssrtest/tc.v
index 7a95b66..20d190f 100644
--- a/mathcomp/ssrtest/tc.v
+++ b/mathcomp/ssrtest/tc.v
@@ -22,7 +22,7 @@ Axiom V : forall A {f : foo A} (x:A), P x -> P (id x).
 
 Lemma test1 (x : nat) : P x -> P (id x).
 Proof.
-move => px.
+move=> px.
 Timeout 2 Fail move/V: px.
 Timeout 2 move/V : (px) => _.
 move/(V nat) : px => H; exact H.
diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v
index 95c62bd..7d90d29 100644
--- a/mathcomp/ssrtest/testmx.v
+++ b/mathcomp/ssrtest/testmx.v
@@ -10,8 +10,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope nat_scope. 
-Local Open Scope ring_scope. 
+Local Open Scope nat_scope.
+Local Open Scope ring_scope.
 
 Section TestMx.
 
diff --git a/mathcomp/ssrtest/wlogletin.v b/mathcomp/ssrtest/wlogletin.v
index 1553621..faeca5c 100644
--- a/mathcomp/ssrtest/wlogletin.v
+++ b/mathcomp/ssrtest/wlogletin.v
@@ -33,8 +33,8 @@ match goal with |- (let fxy0 := f x y in P fxy0 -> P fxy -> P x) => by auto | _
 Qed.
 
 Lemma test4 : forall n m z: bool, n = z -> let x := n in x = m && n -> x = m && n.
-move=> n m z E x H. 
-case: true.   
-  by rewrite  {1 2}E in (x) H |- *.
+move=> n m z E x H.
+case: true.
+  by rewrite {1 2}E in (x) H |- *.
 by rewrite {1}E in x H |- *.
 Qed.