diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
| commit | 0ae5f6871b29d20f48b5df6dab663b5a44162d01 (patch) | |
| tree | 33b11090af2555a91a593f9b919edf83c71557cd /src/CompleteEdwardsCurve/ExtendedCoordinates.v | |
| parent | a0bdb14300aa57eed684992a23a57fd319ef97c0 (diff) | |
remove trailing whitespace from src/
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinates.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 49c5d5041..25af83a0a 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -127,7 +127,7 @@ Module Extended. destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. split; reflexivity. Qed. - + Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. unfold eq. intros x y H x0 y0 H0. @@ -204,10 +204,10 @@ Module Extended. Create HintDb field_homomorphism discriminated. Hint Rewrite <- homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div Ha Hd Hdd |