remove trailing whitespace from src/

14 files changed, 91 insertions, 91 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.
 
diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v
index 52ac91ada..c6f48a0ab 100644
--- a/src/Encoding/EncodingTheorems.v
+++ b/src/Encoding/EncodingTheorems.v
@@ -2,7 +2,7 @@ Require Import Crypto.Spec.Encoding.
 
 Section EncodingTheorems.
   Context {A B : Type} {E : canonical encoding of A as B}.
-  
+
   Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
   Proof.
     intros.
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index 7251ac1e6..41b75e216 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -24,7 +24,7 @@ Section SignBit.
       assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
       omega.
     + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega).
-      pose proof (FieldToZ_range x m_pos).  
+      pose proof (FieldToZ_range x m_pos).
       destruct (FieldToZ x); auto.
       - destruct p; auto.
       - pose proof (Pos2Z.neg_is_neg p); omega.
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index 9a6873bba..33fdb5a17 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -46,7 +46,7 @@ Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB
   : Proper (RA ==> RB) (fun x => Let_In x f).
 Proof. intuition. Qed.
 
-Ltac fold_identity_lambdas := 
+Ltac fold_identity_lambdas :=
   repeat match goal with
            | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in *
            | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in *
@@ -285,7 +285,7 @@ Proof.
   intros.
   pose proof (eqb_eq_dec' eqb eqb_iff a b).
   destruct (eqb a b); eauto.
-Qed. 
+Qed.
 
 Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B}
            (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b)
@@ -308,7 +308,7 @@ Proof. pose proof encoding_valid. congruence. Qed.
 Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B)
       (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b)
       (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b)
-      (P_:B) (Q:T) : 
+      (P_:B) (Q:T) :
   option_rect (fun _ : option T => bool)
                  (fun P : T => T_eqb P Q)
                  false
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 2e65df9bd..9ed7d065e 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -22,19 +22,19 @@ Section ExtendedBaseVector.
   *
   * (x \dot base) * (y \dot base) = (z \dot ext_base)
   *
-  * Then we can separate z into its first and second halves: 
+  * Then we can separate z into its first and second halves:
   *
   * (z \dot ext_base) = (z1 \dot base) + (2 ^ k) * (z2 \dot base)
   *
   * Now, if we want to reduce the product modulo 2 ^ k - c:
-  * 
+  *
   * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + (2 ^ k) * (z2 \dot base) mod (2^k-c)
   * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + c * (z2 \dot base) mod (2^k-c)
   *
   * This sum may be short enough to express using base; if not, we can reduce again.
   *)
   Definition ext_base := base ++ (map (Z.mul (2^k)) base).
-    
+
   Lemma ext_base_positive : forall b, In b ext_base -> b > 0.
   Proof.
     unfold ext_base. intros b In_b_base.
@@ -76,14 +76,14 @@ Section ExtendedBaseVector.
     intuition.
   Qed.
 
-  Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> 
+  Lemma map_nth_default_base_high : forall n, (n < (length base))%nat ->
     nth_default 0 (map (Z.mul (2 ^ k)) base) n =
     (2 ^ k) * (nth_default 0 base n).
   Proof.
     intros.
     erewrite map_nth_default; auto.
   Qed.
-  
+
   Lemma base_good_over_boundary : forall
     (i : nat)
     (l : (i < length base)%nat)
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 9c6a58f9a..ca8c19d18 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -11,9 +11,9 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
   Context `{prm :PseudoMersenneBaseParams}.
-  
+
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
-  
+
   Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
   Local Hint Unfold rep.
@@ -35,13 +35,13 @@ Section PseudoMersenneBase.
 End PseudoMersenneBase.
 
 Section CarryBasePow2.
-  Context `{prm :PseudoMersenneBaseParams}. 
+  Context `{prm :PseudoMersenneBaseParams}.
 
   Definition log_cap i := nth_default 0 limb_widths i.
 
   Definition add_to_nth n (x:Z) xs :=
     set_nth n (x + nth_default 0 xs n) xs.
-  
+
   Definition pow2_mod n i := Z.land n (Z.ones i).
 
   Definition carry_simple i := fun us =>
@@ -54,7 +54,7 @@ Section CarryBasePow2.
     let us' := set_nth i (pow2_mod di (log_cap i)) us in
     add_to_nth   0  (c * (Z.shiftr di (log_cap i))) us'.
 
-  Definition carry i : digits -> digits := 
+  Definition carry i : digits -> digits :=
     if eq_nat_dec i (pred (length base))
     then carry_and_reduce i
     else carry_simple i.
@@ -110,12 +110,12 @@ Section Canonicalization.
     end.
 
   Definition and_term us := if isFull us then max_ones else 0.
-    
+
   Definition freeze us :=
     let us' := carry_full (carry_full (carry_full us)) in
     let and_term := and_term us' in
     (* [and_term] is all ones if us' is full, so the subtractions subtract q overall.
        Otherwise, it's all zeroes, and the subtractions do nothing. *)
      map2 (fun x y => x - y) us' (map (Z.land and_term) modulus_digits).
-   
+
 End Canonicalization.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index c0e942ece..116fe10e5 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -76,7 +76,7 @@ Ltac construct_params prime_modulus len k :=
   | abstract apply prime_modulus
   | abstract brute_force_indices lw].
 
-Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits :=  
+Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits :=
   match limb_widths with
   | nil => nil
   | x :: tail =>
@@ -91,7 +91,7 @@ Ltac subst_precondition := match goal with
   | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H
 end.
 
-Ltac kill_precondition H := 
+Ltac kill_precondition H :=
   forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|];
   subst_precondition.
 
@@ -207,7 +207,7 @@ Section Carries.
     cbv [carry_sequence].
     transitivity (fold_right carry_opt_cps f (List.rev is) us).
     Focus 2.
-    { 
+    {
       assert (forall i, In i (rev is) -> i < length base)%nat as Hr. {
         subst. intros. rewrite <- in_rev in *. auto. }
       remember (rev is) as ris eqn:Heq.
@@ -239,7 +239,7 @@ Section Carries.
     cbv [carry_sequence].
     transitivity (fold_right carry_opt_cps id (List.rev is) us).
     Focus 2.
-    { 
+    {
       assert (forall i, In i (rev is) -> i < length base)%nat as Hr. {
         subst. intros. rewrite <- in_rev in *. auto. }
       remember (rev is) as ris eqn:Heq.
@@ -273,7 +273,7 @@ Section Carries.
     rewrite carry_sequence_opt_cps_correct by assumption.
     apply carry_sequence_rep; eauto using rep_length.
   Qed.
- 
+
   Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat.
   Proof.
     unfold full_carry_chain; rewrite <-base_length; intros.
@@ -502,7 +502,7 @@ Section Multiplication.
     rewrite map_shiftl by apply k_nonneg.
     rewrite c_subst.
     rewrite k_subst.
-    change @map with @map_opt. 
+    change @map with @map_opt.
     change @Z_shiftl_by with @Z_shiftl_by_opt.
     reflexivity.
   Defined.
@@ -640,7 +640,7 @@ Section Canonicalization.
     := proj2_sig (freeze_opt_sig us).
 
   Lemma freeze_opt_canonical: forall us vs x,
-    @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> 
+    @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x ->
     @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x ->
     freeze_opt us = freeze_opt vs.
   Proof.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 562c7d6d4..0462b0f37 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -418,7 +418,7 @@ Section CarryProofs.
 End CarryProofs.
 
 Section CanonicalizationProofs.
-  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat) 
+  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat)
    {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B)
    (c_pos : 0 < c)
    (* on the first reduce step, we add at most one bit of width to the first digit *)
@@ -783,7 +783,7 @@ Section CanonicalizationProofs.
         add_set_nth; [ zero_bounds | ]; apply IHj; auto; omega.
   Qed.
 
-  Ltac carry_seq_lower_bound := 
+  Ltac carry_seq_lower_bound :=
         repeat (intros; eapply carry_sequence_bounds_lower; eauto; carry_length_conditions).
 
   Lemma carry_bounds_lower : forall i us j, (0 < i <= j)%nat -> (length us = length base) ->
@@ -988,7 +988,7 @@ Section CanonicalizationProofs.
     split; (destruct (eq_nat_dec i 0); subst;
       [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth
       | eapply carry_full_2_bounds_succ; eauto; omega]).
-    + zero_bounds. 
+    + zero_bounds.
       - eapply carry_full_2_bounds_0; eauto.
       - eapply carry_full_bounds; eauto; carry_length_conditions.
         carry_seq_lower_bound.
@@ -1097,7 +1097,7 @@ Section CanonicalizationProofs.
           [ apply Z.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto;
           ring_simplify | ]; omega.
     + rewrite carry_unaffected_low by carry_length_conditions.
-      assert (0 < S i < length base)%nat by omega. 
+      assert (0 < S i < length base)%nat by omega.
       intuition; right.
       apply carry_carry_done_done; try solve [carry_length_conditions].
       assumption.
@@ -1123,7 +1123,7 @@ Section CanonicalizationProofs.
     unfold carry, carry_and_reduce; break_if; try omega; intros.
     add_set_nth.
     split.
-    + zero_bounds. 
+    + zero_bounds.
       - eapply carry_full_2_bounds_same; eauto; omega.
       - eapply carry_carry_full_2_bounds_0_lower; eauto; omega.
     + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))).
@@ -1138,12 +1138,12 @@ Section CanonicalizationProofs.
         ring_simplify.
         apply carry_full_2_bounds_same; auto.
       - match goal with H0 : (pred (length base) < length base)%nat,
-                        H : carry_done _ |- _ => 
+                        H : carry_done _ |- _ =>
           destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end.
         ring_simplify.
         apply shiftr_eq_0_max_bound; auto.
         assert (0 < length base)%nat as zero_lt_length by omega.
-        match goal with H : carry_done _ |- _ => 
+        match goal with H : carry_done _ |- _ =>
           destruct (H 0%nat zero_lt_length) end.
        assumption.
   Qed.
@@ -1277,7 +1277,7 @@ Section CanonicalizationProofs.
   Local Hint Resolve carry_full_3_length.
 
   Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
-    nth_default d (map2 f ls1 ls2) i = 
+    nth_default d (map2 f ls1 ls2) i =
       if lt_dec i (min (length ls1) (length ls2))
       then f (nth_default d1 ls1 i) (nth_default d2 ls2 i)
       else d.
@@ -1487,7 +1487,7 @@ Section CanonicalizationProofs.
     replace (S (length base - 1)) with (length base) by omega.
     reflexivity.
   Qed.
-    
+
   Lemma carry_done_modulus_digits : carry_done modulus_digits.
   Proof.
     apply carry_done_bounds; [apply modulus_digits_length | ].
@@ -1660,7 +1660,7 @@ Section CanonicalizationProofs.
   Proof.
     unfold isFull; intros; auto using isFull'_true_iff.
   Qed.
-  
+
   Definition minimal_rep us := BaseSystem.decode base us = (BaseSystem.decode base us) mod modulus.
 
   Fixpoint compare' us vs i :=
@@ -1813,7 +1813,7 @@ Section CanonicalizationProofs.
     intros.
     destruct (Z_dec (nth_default 0 us n) (nth_default 0 vs n)) as [[?|Hgt]|?]; try congruence.
     + etransitivity; try apply Z_compare_decode_step_lt; auto.
-    + match goal with |- (?a ?= ?b) = (?c ?= ?d) => 
+    + match goal with |- (?a ?= ?b) = (?c ?= ?d) =>
         rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end.
       apply CompOpp_inj; rewrite !CompOpp_involutive.
       apply gt_lt_symmetry in Hgt.
@@ -1923,11 +1923,11 @@ Section CanonicalizationProofs.
       - rewrite nth_default_modulus_digits in *.
         repeat (break_if; try omega).
         * subst.
-          match goal with H : isFull' _ _ _ = true |- _ => 
+          match goal with H : isFull' _ _ _ = true |- _ =>
             apply isFull'_lower_bound_0 in H end.
           apply Z.compare_ge_iff.
           omega.
-        * match goal with H : isFull' _ _ _ = true |- _ => 
+        * match goal with H : isFull' _ _ _ = true |- _ =>
             apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_bound] end.
           specialize (eq_max_bound j).
           omega.
@@ -2065,7 +2065,7 @@ Section CanonicalizationProofs.
     us = vs.
   Proof.
    intros.
-   match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ => 
+   match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ =>
      pose proof (rep_decode_mod _ _ _ Hrep1 Hrep2) as eqmod end.
    repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin;
      rewrite <- Hmin in eqmod; clear Hmin end.
@@ -2076,7 +2076,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma freeze_canonical : forall us vs x,
-    pre_carry_bounds us -> rep us x -> 
+    pre_carry_bounds us -> rep us x ->
     pre_carry_bounds vs -> rep vs x ->
     freeze us = freeze vs.
   Proof.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 10bbdf33d..49b1875ce 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -32,7 +32,7 @@ Section PseudoMersenneBaseParamProofs.
     unfold value in *.
     congruence.
   Qed.
-  
+
   Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat ->
     nth_error base i = Some b ->
     nth_error limb_widths i = Some w ->
@@ -45,7 +45,7 @@ Section PseudoMersenneBaseParamProofs.
     case_eq i; intros; subst.
     + subst; apply nth_error_first in nth_err_w.
       apply nth_error_first in nth_err_b; subst.
-      apply map_nth_error. 
+      apply map_nth_error.
       case_eq l; intros; subst; [simpl in *; omega | ].
       unfold base_from_limb_widths; fold base_from_limb_widths.
       reflexivity.
@@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs.
     apply nth_error_first in H.
     subst; eauto.
   Qed.
-  
+
   Lemma sum_firstn_succ : forall l i x,
     nth_error l i = Some x ->
     sum_firstn l (S i) = x + sum_firstn l i.
@@ -117,7 +117,7 @@ Section PseudoMersenneBaseParamProofs.
     induction i; intros.
     + unfold base, sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity.
       intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega.
-    + 
+    +
       assert (i < length base)%nat as lt_i_length by omega.
       specialize (IHi lt_i_length).
       rewrite base_length in lt_i_length.
@@ -138,7 +138,7 @@ Section PseudoMersenneBaseParamProofs.
         apply limb_widths_nonneg.
         eapply nth_error_value_In; eauto.
   Qed.
-  
+
   Lemma nth_default_base : forall d i, (i < length base)%nat ->
     nth_default d base i = 2 ^ (sum_firstn limb_widths i).
   Proof.
@@ -178,7 +178,7 @@ Section PseudoMersenneBaseParamProofs.
     + rewrite base_length in *; apply limb_widths_match_modulus; assumption.
   Qed.
 
-  Lemma base_succ : forall i, ((S i) < length base)%nat -> 
+  Lemma base_succ : forall i, ((S i) < length base)%nat ->
     nth_default 0 base (S i) mod nth_default 0 base i = 0.
   Proof.
     intros.
@@ -226,7 +226,7 @@ Section PseudoMersenneBaseParamProofs.
    Proof.
      unfold base; case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity].
    Qed.
- 
+
    Lemma base_good : forall i j : nat,
                 (i + j < length base)%nat ->
                 let b := nth_default 0 base in
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 5df36e295..88388ee0a 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -24,12 +24,12 @@ Module E.
         nonsquare_d : forall x, x^2 <> d
       }.
     Context `{twisted_edwards_params}.
-  
+
     Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }.
     Definition coordinates (P:point) : (F*F) := proj1_sig P.
 
     Program Definition zero : point := (0, 1).
-    
+
     Program Definition add (P1 P2:point) : point := exist _ (
       let (x1, y1) := coordinates P1 in
       let (x2, y2) := coordinates P2 in
@@ -47,7 +47,7 @@ Module E.
       end.
   End TwistedEdwardsCurves.
 End E.
-  
+
 Delimit Scope E_scope with E.
 Infix "+" := E.add : E_scope.
 Infix "*" := E.mul : E_scope.
\ No newline at end of file
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index bd8a095dd..2c7097207 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -26,7 +26,7 @@ Section EdDSA.
         {PointEncoding : canonical encoding of E as Word.word b} (* wire format *)
         {FlEncoding : canonical encoding of { n | n < l } as Word.word b}
     :=
-      { 
+      {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
 
         EdDSA_c_valid : c = 2 \/ c = 3;
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 9a9ce9a06..0426c0834 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -18,7 +18,7 @@ Proof.
 intros. induction n; boring.
 Qed.
 
-Ltac nth_tac' := 
+Ltac nth_tac' :=
   intros; simpl in *; unfold error,value in *; repeat progress (match goal with
     | [  |- context[nth_error nil ?n] ] => rewrite nth_error_nil_error
     | [ H: ?x = Some _  |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x
@@ -79,10 +79,10 @@ Proof.
   reflexivity.
   nth_tac'.
   pose proof (nth_error_error_length A n l H0).
-  omega.  
+  omega.
 Qed.
 
-Ltac nth_tac := 
+Ltac nth_tac :=
   repeat progress (try nth_tac'; try (match goal with
     | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H
     | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H
@@ -191,7 +191,7 @@ Proof.
 Qed.
 
 Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
-  set_nth n x xs = 
+  set_nth n x xs =
   if lt_dec n (length xs)
   then splice_nth n x xs
   else xs.
@@ -210,7 +210,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
     end.
 Proof.
   (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypotheses at once *)
-  induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac; 
+  induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac;
     try (f_equal; specialize (IHn x xs ys ); rewrite H in IHn; rewrite <- IHn);
     try (specialize (nth_error_value_length _ _ _ _ H); omega).
   assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto).
@@ -330,7 +330,7 @@ Proof.
   intros.
   rewrite firstn_app_inleft; auto using firstn_all; omega.
 Qed.
-    
+
 Lemma skipn_app_sharp : forall {A} n (l l': list A),
   length l = n ->
   skipn n (l ++ l') = l'.
@@ -422,7 +422,7 @@ Proof.
     right; repeat eexists; auto.
   }
 Qed.
- 
+
 Lemma nil_length0 : forall {T}, length (@nil T) = 0%nat.
 Proof.
   auto.
@@ -512,7 +512,7 @@ Ltac nth_error_inbounds :=
   match goal with
   | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
     case_eq (nth_error xs i);
-    match goal with 
+    match goal with
       | [ |- forall _, nth_error xs i = Some _ -> _ ] =>
           let x := fresh "x" in
           let H := fresh "H" in