aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-01 23:59:55 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 00:00:09 -0400
commitd3135a69f653034f07b7657486f926a7a20ef3ee (patch)
treee163e017643c1bc8c877ecefaa43299c458d232e /src/Algebra
parent3f11f57487ce9e913b36271cee2f8b6b695945cf (diff)
Strip trailing whitespace
With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
Diffstat (limited to 'src/Algebra')
-rw-r--r--src/Algebra/Field_test.v2
-rw-r--r--src/Algebra/Group.v2
-rw-r--r--src/Algebra/ScalarMult.v2
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.