Strip trailing whitespace

With
```bash
bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh
```

28 files changed, 56 insertions, 56 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.
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index b86ac09b9..d61ff5ba4 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -837,7 +837,7 @@ Module B.
 
     Section Select.
       Context {weight : nat -> Z}.
-      
+
       Definition select_cps {n} (mask cond:Z) (p:tuple Z n)
                  {T} (f:tuple Z n->T) :=
         dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f.
diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v
index b27ffd16d..3063d3a51 100644
--- a/src/Arithmetic/ModularArithmeticPre.v
+++ b/src/Arithmetic/ModularArithmeticPre.v
@@ -136,4 +136,4 @@ Next Obligation.
   replace (Z.succ (m - 2)) with (m-1) by omega.
   rewrite (Zmod_small 1) by omega.
   apply (fermat_little m Hm a Ha).
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 990aa9dc8..8f9277f35 100644
--- a/src/Arithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -17,10 +17,10 @@ Module F.
     lazy iota beta delta [F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *;
     try apply eqsig_eq;
     pull_Zmod.
-  
+
   (* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *)
   Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.
-  
+
   Global Instance commutative_ring_modulo m
     : @Algebra.Hierarchy.commutative_ring (F m) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul.
   Proof.
@@ -48,14 +48,14 @@ Module F.
     Lemma eq_of_Z_iff : forall x y : Z, x mod m = y mod m <-> F.of_Z m x = F.of_Z m y.
     Proof using Type. split; unwrap_F; congruence. Qed.
 
-    
+
     Lemma to_Z_of_Z : forall z, F.to_Z (F.of_Z m z) = z mod m.
     Proof using Type. unwrap_F; trivial. Qed.
 
     Lemma of_Z_to_Z x : F.of_Z m (F.to_Z x) = x :> F m.
     Proof using Type. unwrap_F; congruence. Qed.
 
-    
+
     Lemma of_Z_mod : forall x, F.of_Z m x = F.of_Z m (x mod m).
     Proof using Type. unwrap_F; trivial. Qed.
 
@@ -95,7 +95,7 @@ Module F.
     Lemma to_Z_mul : forall x y : F m,
         F.to_Z (x * y) = ((F.to_Z x * F.to_Z y) mod m)%Z.
     Proof using Type. unwrap_F; trivial. Qed.
-    
+
     Lemma of_Z_sub x y : F.of_Z _ (x - y) = F.of_Z _ x - F.of_Z _ y :> F m.
     Proof using Type. unwrap_F. trivial. Qed.
 
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index c253752c5..edab4e065 100644
--- a/src/Arithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -95,7 +95,7 @@ Module F.
       rewrite <-H in q_3mod4; discriminate.
     Qed.
     Local Hint Resolve two_lt_q_3mod4.
-    
+
     Lemma sqrt_3mod4_correct (x:F q) :
       ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F.
     Proof using Type*.
@@ -130,7 +130,7 @@ Module F.
                            constants [F.is_constant],
                            div (F.morph_div_theory q),
                            power_tac (F.power_theory q) [F.is_pow_constant]).
-    
+
     (* Any nonsquare element raised to (q-1)/4 (real implementations use 2 ^ ((q-1)/4) )
        would work for sqrt_minus1 *)
     Context (sqrt_minus1 : F q) (sqrt_minus1_valid : sqrt_minus1 * sqrt_minus1 = F.opp 1).
@@ -241,7 +241,7 @@ Module F.
   Module Iso.
     Section IsomorphicRings.
       Context {q:positive} {prime_q:prime q} {two_lt_q:2 < Z.pos q}.
-      Context 
+      Context
         {H : Type} {eq : H -> H -> Prop} {zero one : H}
         {opp : H -> H} {add sub mul : H -> H -> H}
         {phi : F q -> H} {phi' : H -> F q}
@@ -256,7 +256,7 @@ Module F.
         {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}.
       Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)).
       Definition div x y := mul (inv y) x.
-      
+
       Lemma ring :
         @Algebra.Hierarchy.ring H eq zero one opp add sub mul
         /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index 650cd7bcf..a66c268b0 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -49,14 +49,14 @@ a [tuple Z n] as output. This operation is called "compact".
 As an example, let's compact the product of 571 and 645 in base 10.
 At first, the partial products look like this:
 
-      
-                   1*6         
+
+                   1*6
             1*4    7*4     7*6
      1*5    7*5    5*5     5*4      5*6
     ------------------------------------
        1     10    100    1000    10000
-                   
-                     6         
+
+                     6
               4     28      42
        5     35     25      20       30
     ------------------------------------
@@ -75,7 +75,7 @@ bit. We add a 0 to the next column and continue.
      {carry_acc = 0; output=(5,)}
      STEP [4,35] (4 + 35 = 39)
      {carry_acc = 3; output=(9,5)}
-     
+
 This time, we have a carry. We add it to the third column and process
 that:
 
@@ -93,7 +93,7 @@ columns:
      {carry_acc = 4; output=(8,9,5)}
      STEP [4,20] (4 + 20 = 24)
      {carry_acc = 6; output=(4,8,9,5)}
-     
+
      STEP [6,30] (6 + 30 = 36)
      {carry_acc = 3; output=(6,4,8,9,5)}
 
@@ -213,7 +213,7 @@ Module Columns.
                | _ => progress (autorewrite with uncps push_id cancel_pair in * )
                | _ => progress break_match; try discriminate
                | _ => reflexivity
-               | _ => f_equal; ring 
+               | _ => f_equal; ring
                end.
     Qed. Hint Rewrite compact_digit_mod : div_mod.
 
@@ -229,9 +229,9 @@ Module Columns.
                | _ => progress (autorewrite with uncps push_id cancel_pair in * )
                | _ => progress break_match; try discriminate
                | _ => reflexivity
-               | _ => f_equal; ring 
+               | _ => f_equal; ring
                end.
-      assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero. 
+      assert (weight (S i) / weight i <> 0) by auto using Z.positive_is_nonzero.
       match goal with |- _ = (?a + ?X) / ?D =>
                       transitivity  ((a + X mod D + D * (X / D)) / D);
                         [| rewrite (Z.div_mod'' X D) at 3; f_equal; auto; ring]
@@ -279,7 +279,7 @@ Module Columns.
         with (fun i s a => compact_digit i (s :: a)).
 
       apply mapi_with'_linvariant; [|tauto].
-      
+
       clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv].
       pose proof (weight_positive n). pose proof (weight_divides n).
       autorewrite with push_basesystem_eval.
@@ -292,8 +292,8 @@ Module Columns.
                | _ => rewrite map_left_append
                | _ => rewrite B.Positional.eval_left_append
                | _ => rewrite weight_0, ?Z.div_1_r, ?Z.mod_1_r
-               | _ => rewrite Hdiv 
-               | _ => rewrite Hmod 
+               | _ => rewrite Hdiv
+               | _ => rewrite Hmod
                | _ => progress subst
                | _ => progress autorewrite with natsimplify cancel_pair push_basesystem_eval
                | _ => solve [split; ring_simplify; f_equal; ring]
@@ -424,7 +424,7 @@ Module Columns.
         (fun nq => B.Positional.to_associational_cps weight nq
         (fun Q => from_associational_cps weight n (P++Q)
         (fun R => compact_cps (div:=div) (modulo:=modulo) (add_get_carry:=add_get_carry) weight R f)))).
-   
+
     End Wrappers.
 End Columns.
 Hint Unfold
@@ -491,8 +491,8 @@ Section Freeze.
   Qed.
   Hint Rewrite @eval_conditional_add using (omega || assumption)
     : push_basesystem_eval.
-    
-    
+
+
   (*
     The input to [freeze] should be less than 2*m (this can probably
     be accomplished by a single carry_reduce step, for most moduli).
@@ -552,7 +552,7 @@ Section Freeze.
       by (pose proof (Z.div_small (y - (s-c)) s); omega).
       f_equal. ring. }
   Qed.
-  
+
   Lemma eval_freeze {n} c mask m p
         (n_nonzero:n<>0%nat)
         (Hc : 0 < B.Associational.eval c < weight n)
@@ -589,7 +589,7 @@ Section Freeze.
   Qed.
 End Freeze.
 
-  
+
 (*
 (* Just some pretty-printing *)
 Local Notation "fst~ a" := (let (x,_) := a in x) (at level 40, only printing).
diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v
index 244acc9b5..9f5d5cfab 100644
--- a/src/Curves/Edwards/Pre.v
+++ b/src/Curves/Edwards/Pre.v
@@ -43,4 +43,4 @@ Section Edwards.
     Lemma onCurve_add : onCurve ((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)).
     Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed.
   End Addition.
-End Edwards.
\ No newline at end of file
+End Edwards.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index 70e8a3f6f..bfd7dce60 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -62,4 +62,4 @@ Module M.
       Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
     End MontgomeryWeierstrass.
   End MontgomeryCurve.
-End M.
\ No newline at end of file
+End M.
diff --git a/src/Curves/Montgomery/AffineInstances.v b/src/Curves/Montgomery/AffineInstances.v
index ef5ccd578..049a7695b 100644
--- a/src/Curves/Montgomery/AffineInstances.v
+++ b/src/Curves/Montgomery/AffineInstances.v
@@ -19,7 +19,7 @@ Module M.
     Local Notation "0" := Fzero.
     Local Notation "1" := Fone.
     Local Notation "4" := (1+1+1+1).
-      
+
     Global Instance MontgomeryWeierstrassIsomorphism
            {a b: F}
            (b_nonzero : b <> 0)
@@ -40,7 +40,7 @@ Module M.
         (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero))
         M.zero
         (M.opp(b_nonzero:=b_nonzero))
-        
+
         (M.of_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero))
         (M.to_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero)).
     Proof.
diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v
index 4601c3b66..588605c35 100644
--- a/src/Curves/Montgomery/AffineProofs.v
+++ b/src/Curves/Montgomery/AffineProofs.v
@@ -13,7 +13,7 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}.
-      
+
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -74,7 +74,7 @@ Module M.
         (M.add(char_ge_3:=_3)(b_nonzero:=_4))
         M.zero
         (M.opp(b_nonzero:=_7))
-        
+
         (M.of_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_5))
         (M.to_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_6)).
     Proof.
diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v
index 3a48bf998..cdcb1bec7 100644
--- a/src/Curves/Weierstrass/Affine.v
+++ b/src/Curves/Weierstrass/Affine.v
@@ -17,4 +17,4 @@ Module W.
       cbv [W.coordinates]; break_match; trivial; fsatz.
     Qed.
   End W.
-End W.
\ No newline at end of file
+End W.
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v
index 3401d7b31..2faac22eb 100644
--- a/src/Curves/Weierstrass/AffineProofs.v
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -35,7 +35,7 @@ Module W.
            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *)
            {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)}
       : commutative_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
-    Proof using Type. 
+    Proof using Type.
       Time
         cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig];
           repeat match goal with
diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v
index a54bc483f..3f426e98b 100644
--- a/src/LegacyArithmetic/BaseSystem.v
+++ b/src/LegacyArithmetic/BaseSystem.v
@@ -36,4 +36,4 @@ Section BaseSystem.
   Definition decode' bs u  := fold_right accumulate 0 (combine u bs).
   Definition decode := decode' base.
   Definition mul_each u := map (Z.mul u).
-End BaseSystem.
\ No newline at end of file
+End BaseSystem.
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index 9a06109d1..b87df814d 100644
--- a/src/LegacyArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -130,4 +130,4 @@ Section BaseSystemProofs.
             rewrite plus_0_r in *;
             congruence); simpl in HH; congruence. }
   Qed.
-End BaseSystemProofs.
\ No newline at end of file
+End BaseSystemProofs.
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index 681f0b0a9..35540f39a 100644
--- a/src/LegacyArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -552,4 +552,4 @@ Section UniformBase.
     rewrite decode_shift_app by auto using uniform_limb_widths_nonneg.
     reflexivity.
   Qed.
-End UniformBase.
\ No newline at end of file
+End UniformBase.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 83e5645d5..9cde8d004 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -52,4 +52,4 @@ End E.
 Delimit Scope E_scope with E.
 Infix "=" := E.eq : E_scope.
 Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope.
\ No newline at end of file
+Infix "*" := E.mul : E_scope.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index b8526bb0e..56d5c1bf0 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -54,11 +54,11 @@ Section Ed25519.
 
   Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *)
     @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0)
-                  (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) 
+                  (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q)
                   (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two).
   Proof. intros p ?.
          edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst.
-         { admit. (* 
+         { admit. (*
            p : BinNums.positive
            H : BinPos.Pos.le p (BinNat.N.succ_pos BinNat.N.one)
            ============================
@@ -89,7 +89,7 @@ Section Ed25519.
           (l:=l) (b:=b) (n:=n) (c:=c)
           (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
   Proof using Type.
-    split; 
+    split;
       match goal with
       | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *)
       | _ => exact _
diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v
index 15ca468c1..a4fed8dd4 100644
--- a/src/Spec/Test/X25519.v
+++ b/src/Spec/Test/X25519.v
@@ -19,4 +19,4 @@ Proof. vm_decide_no_check. Qed.
 Example testvector_two : F.to_Z (monty
    35156891815674817266734212754503633747128614016119564763269015315466259359304%N
    (F.of_Z _ 8883857351183929894090759386610649319417338800022198945255395922347792736741%Z)) = 39566196721700740701373067725336211924689549479508623342842086701180565506965%Z.
-Proof. vm_decide_no_check. Qed.
\ No newline at end of file
+Proof. vm_decide_no_check. Qed.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index fc7c64198..9a3a9185d 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -41,7 +41,7 @@ Module W.
     Program Definition zero : point := ∞.
 
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Notation "2" := (1+1). Local Notation "3" := (1+2). 
+    Local Notation "2" := (1+1). Local Notation "3" := (1+2).
 
     Program Definition add (P1 P2:point) : point :=
       match coordinates P1, coordinates P2 return F*F+∞ with
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 438f8305e..d9e801a0c 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -254,7 +254,7 @@ Section Ops51.
 
   Hint Opaque freeze : uncps.
   Hint Rewrite freeze_id : uncps.
-  
+
   Definition freeze_sig :
     {freeze : (Z^sz -> Z^sz)%type |
      forall a : Z^sz,
@@ -281,7 +281,7 @@ Section Ops51.
    cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect].
    reflexivity.
   Defined.
-  
+
   Definition ring_51 :=
     (Ring.ring_by_isomorphism
          (F := F m)
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index c09edc891..41b21feb7 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -288,4 +288,4 @@ Module Tuple.
 End Tuple.
 Hint Rewrite @Tuple.map_cps_correct : uncps.
 Hint Rewrite @Tuple.mapi_with_cps_correct @Tuple.mapi_with'_cps_correct
-     using (intros; autorewrite with uncps; auto): uncps.
\ No newline at end of file
+     using (intros; autorewrite with uncps; auto): uncps.
diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v
index 8ccb7d119..12893cd75 100644
--- a/src/Util/Factorize.v
+++ b/src/Util/Factorize.v
@@ -70,4 +70,4 @@ Lemma product_factorize_or_fail (n:N) (factors:list N)
       (H:Logic.eq (factorize_or_fail n) (Some factors))
   : Logic.eq (List.fold_right N.mul 1%N factors) n.
 Proof.  cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?;
-          try apply N.eqb_eq; congruence. Qed.
\ No newline at end of file
+          try apply N.eqb_eq; congruence. Qed.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 1faa1da95..d76be63aa 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -117,7 +117,7 @@ Module N.
       replace (Z.of_nat 2) with 2%Z by reflexivity.
       omega.
     Qed.
- 
+
     Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x).
     Lemma combine_ZNWord : forall sz1 sz2 z1 z2,
         (0 <= Z.of_nat sz1)%Z ->
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 2ccb0455f..74fe96d6b 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -304,4 +304,4 @@ Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z.
 Proof.
   rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1.
   apply Z_div_mod_eq; reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
index 7dc654ec3..d6b63b38f 100644
--- a/src/Util/Relations.v
+++ b/src/Util/Relations.v
@@ -56,4 +56,4 @@ Global Instance Symmetric_not {T:Type} (R:T->T->Prop)
        {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)).
 Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed.
 
-Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed.
\ No newline at end of file
+Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed.
diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v
index 0166ce6f4..fa9235a0b 100644
--- a/src/Util/ZUtil/Zselect.v
+++ b/src/Util/ZUtil/Zselect.v
@@ -13,4 +13,4 @@ Module Z.
       try reflexivity; try discriminate.
     rewrite <-Z.eqb_neq in *; congruence.
   Qed.
-End Z.
\ No newline at end of file
+End Z.