running semi-automated linting on the whole library

1 files changed, 7 insertions, 7 deletions

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).