3 files changed, 3 insertions, 3 deletions
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 59ca72c6b..149a6373e 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -92,4 +92,4 @@ Module _fsatz_test.
       : x7 = x9 /\ y7 = y9.
     Proof using Type*. fsatz_prepare_hyps; split; fsatz. Qed.
   End _test.
-End _fsatz_test.
-\ No newline at end of file
+End _fsatz_test.
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 27c45dcec..01325de3f 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -196,4 +196,4 @@ Section CommutativeGroupByIsomorphism.
            | _ => solve [ eauto ]
            end.
   Qed.
-End CommutativeGroupByIsomorphism.
-\ No newline at end of file
+End CommutativeGroupByIsomorphism.
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index f52fc93ee..034ed4d4c 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -89,4 +89,4 @@ End ScalarMultHomomorphism.
 
 Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
   : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
-Proof. split; try exact _; intros; reflexivity. Qed.
-\ No newline at end of file
+Proof. split; try exact _; intros; reflexivity. Qed.