remove trailing whitespace from src/

3 files changed, 33 insertions, 33 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 89984027f..99029a671 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -23,10 +23,10 @@ Module E.
     Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d).
 
     Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)).
-  
+
     Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q).
     Infix "=" := eq : E_scope.
-  
+
     (* TODO: decide whether we still want something like this, then port
     Local Ltac t :=
       unfold point_eqb;
@@ -41,41 +41,41 @@ Module E.
         | [H: _ |- _ ] => apply F_eqb_eq in H
         | _ => rewrite F_eqb_refl
         end; eauto.
-  
+
     Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2.
     Proof.
       t.
     Qed.
-  
+
     Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true.
     Proof.
       t.
     Qed.
-  
+
     Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2.
     Proof.
       intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
       apply point_eqb_complete in H0; congruence.
     Qed.
-  
+
     Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false.
     Proof.
       intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
       apply point_eqb_sound in Hneq. congruence.
     Qed.
-  
+
     Lemma point_eqb_refl : forall p, point_eqb p p = true.
     Proof.
       t.
     Qed.
-  
+
     Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}.
       destruct (point_eqb p1 p2) eqn:H; match goal with
                                         | [ H: _ |- _ ] => apply point_eqb_sound in H
                                         | [ H: _ |- _ ] => apply point_eqb_neq in H
                                         end; eauto.
     Qed.
-  
+
     Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false.
     Proof.
       intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
@@ -86,7 +86,7 @@ Module E.
     Lemma decide_and  : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}.
     Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed.
 
-    Ltac destruct_points := 
+    Ltac destruct_points :=
       repeat match goal with
              | [ p : point |- _ ] =>
                let x := fresh "x" p in
@@ -104,7 +104,7 @@ Module E.
     Local Hint Resolve nonsquare_d.
     Local Hint Resolve @edwardsAddCompletePlus.
     Local Hint Resolve @edwardsAddCompleteMinus.
-  
+
     Program Definition opp (P:point) : point :=
       exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
     Solve All Obligations using intros; destruct_points; simpl; field_algebra.
@@ -158,14 +158,14 @@ Module E.
     Section PointCompression.
       Local Notation "x ^2" := (x*x).
       Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)).
-      
+
       Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0.
       Proof.
         intros ? eq_zero.
         destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero.
         destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra.
       Qed.
-      
+
       Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y).
       Proof.
         unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero.
@@ -189,10 +189,10 @@ Module E.
     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
       : field_homomorphism.
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
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 397a6259c..5314ee37c 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -16,14 +16,14 @@ Section Pre.
   Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}.
   Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}.
   Context {char_gt_2 : 1+1 <> 0}.
-  
+
   (* the canonical definitions are in Spec *)
   Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
   Definition unifiedAdd' (P1' P2':F*F) : F*F :=
     let (x1, y1) := P1' in
     let (x2, y2) := P2' in
     pair (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-  
+
   Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
 
   Lemma edwardsAddComplete' x1 y1 x2 y2 :
@@ -44,13 +44,13 @@ Section Pre.
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
     onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0.
   Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
-  
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0.
   Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
-  
+
   Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed.
-  
+
   Lemma unifiedAdd'_onCurve : forall P1 P2,
     onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
   Proof.
@@ -71,7 +71,7 @@ Section RespectsFieldHomomorphism.
 
   Let phip  := fun (P':F*F) => let (x, y) := P' in (phi x, phi y).
 
-  Let eqp := fun (P1' P2':K*K) => 
+  Let eqp := fun (P1' P2':K*K) =>
     let (x1, y1) := P1' in
     let (x2, y2) := P2' in
     and (eq x1 x2) (eq y1 y2).
@@ -79,11 +79,11 @@ Section RespectsFieldHomomorphism.
   Create HintDb field_homomorphism discriminated.
   Hint Rewrite
        homomorphism_one
-       homomorphism_add 
-       homomorphism_sub 
-       homomorphism_mul 
-       homomorphism_div 
-       a_ok 
+       homomorphism_add
+       homomorphism_sub
+       homomorphism_mul
+       homomorphism_div
+       a_ok
        d_ok
        : field_homomorphism.