1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 5a2cc9695..6d3dc02a9 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -18,26 +18,26 @@ Declare ML Module "ascii_syntax_plugin".
 (** * Definition of ascii characters *)
 
 (** Definition of ascii character as a 8 bits constructor *)
- 
+
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
 Delimit Scope char_scope with char.
 Bind Scope char_scope with ascii.
- 
+
 Definition zero := Ascii false false false false false false false false.
- 
+
 Definition one := Ascii true false false false false false false false.
- 
+
 Definition app1 (f : bool -> bool) (a : ascii) :=
   match a with
     | Ascii a1 a2 a3 a4 a5 a6 a7 a8 =>
       Ascii (f a1) (f a2) (f a3) (f a4) (f a5) (f a6) (f a7) (f a8)
   end.
- 
+
 Definition app2 (f : bool -> bool -> bool) (a b : ascii) :=
   match a, b with
     | Ascii a1 a2 a3 a4 a5 a6 a7 a8, Ascii b1 b2 b3 b4 b5 b6 b7 b8 =>
-      Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4) 
+      Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4)
       (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8)
   end.
 
@@ -47,7 +47,7 @@ Definition shift (c : bool) (a : ascii) :=
   end.
 
 (** Definition of a decidable function that is effective *)
- 
+
 Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
   decide equality; apply bool_dec.
 Defined.
@@ -57,7 +57,7 @@ Defined.
 (** Auxillary function that turns a positive into an ascii by
    looking at the last n bits, ie z mod 2^n *)
 
-Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) 
+Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive)
   (n : nat) {struct n} : ascii :=
   match n with
     | O => res
@@ -72,7 +72,7 @@ Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive)
 
 (** Function that turns a positive into an ascii by
     looking at the last 8 bits, ie a mod 8 *)
- 
+
 Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8.
 
 (** Function that turns a Peano number into an ascii by converting it
@@ -83,7 +83,7 @@ Definition ascii_of_nat (a : nat) :=
     | O => zero
     | S a' => ascii_of_pos (P_of_succ_nat a')
   end.
- 
+
 (** The opposite function *)
 
 Definition nat_of_ascii (a : ascii) : nat :=
@@ -103,7 +103,7 @@ Definition nat_of_ascii (a : ascii) : nat :=
       + (if a2 then 1 else 0))
     + (if a1 then 1 else 0).
 
-Theorem ascii_nat_embedding : 
+Theorem ascii_nat_embedding :
   forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
 Proof.
   destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
@@ -124,7 +124,7 @@ Qed.
   Notice that the ascii characters of code >= 128 do not denote
   stand-alone utf8 characters so that only the notation "nnn" is
   available for them (unless your terminal is able to represent them,
-  which is typically not the case in coqide). 
+  which is typically not the case in coqide).
 *)
 
 Open Local Scope char_scope.