Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 32 insertions, 32 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.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 7d6696b78..82a60c189 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -18,7 +18,7 @@ Declare ML Module "string_syntax_plugin".
 (** *** Definition of strings *)
 
 (** Implementation of string as list of ascii characters *)
- 
+
 Inductive string : Set :=
   | EmptyString : string
   | String : ascii -> string -> string.
@@ -48,7 +48,7 @@ where "s1 ++ s2" := (append s1 s2) : string_scope.
 (******************************)
 (** Length                    *)
 (******************************)
- 
+
 Fixpoint length (s : string) : nat :=
   match s with
   | EmptyString => 0
@@ -58,7 +58,7 @@ Fixpoint length (s : string) : nat :=
 (******************************)
 (** Nth character of a string *)
 (******************************)
- 
+
 Fixpoint get (n : nat) (s : string) {struct s} : option ascii :=
   match s with
   | EmptyString => None
@@ -69,7 +69,7 @@ Fixpoint get (n : nat) (s : string) {struct s} : option ascii :=
   end.
 
 (** Two lists that are identical through get are syntactically equal *)
- 
+
 Theorem get_correct :
   forall s1 s2 : string, (forall n : nat, get n s1 = get n s2) <-> s1 = s2.
 Proof.
@@ -90,7 +90,7 @@ rewrite H1; auto.
 Qed.
 
 (** The first elements of [s1 ++ s2] are the ones of [s1] *)
- 
+
 Theorem append_correct1 :
  forall (s1 s2 : string) (n : nat),
  n < length s1 -> get n s1 = get n (s1 ++ s2).
@@ -103,7 +103,7 @@ apply lt_S_n; auto.
 Qed.
 
 (** The last elements of [s1 ++ s2] are the ones of [s2] *)
- 
+
 Theorem append_correct2 :
  forall (s1 s2 : string) (n : nat),
  get n s2 = get (n + length s1) (s1 ++ s2).
@@ -120,7 +120,7 @@ Qed.
 (** [substring n m s] returns the substring of [s] that starts
     at position [n] and of length [m];
     if this does not make sense it returns [""] *)
- 
+
 Fixpoint substring (n m : nat) (s : string) {struct s} : string :=
   match n, m, s with
   | 0, 0, _ => EmptyString
@@ -131,7 +131,7 @@ Fixpoint substring (n m : nat) (s : string) {struct s} : string :=
   end.
 
 (** The substring is included in the initial string *)
- 
+
 Theorem substring_correct1 :
  forall (s : string) (n m p : nat),
  p < m -> get p (substring n m s) = get (p + n) s.
@@ -149,7 +149,7 @@ intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl in |- *; auto.
 Qed.
 
 (** The substring has at most [m] elements *)
- 
+
 Theorem substring_correct2 :
  forall (s : string) (n m p : nat), m <= p -> get p (substring n m s) = None.
 Proof.
@@ -167,7 +167,7 @@ Qed.
 (** *** Test functions *)
 
 (** Test if [s1] is a prefix of [s2] *)
- 
+
 Fixpoint prefix (s1 s2 : string) {struct s2} : bool :=
   match s1 with
   | EmptyString => true
@@ -184,7 +184,7 @@ Fixpoint prefix (s1 s2 : string) {struct s2} : bool :=
 
 (** If [s1] is a prefix of [s2], it is the [substring] of length
     [length s1] starting at position [O] of [s2] *)
- 
+
 Theorem prefix_correct :
  forall s1 s2 : string,
  prefix s1 s2 = true <-> substring 0 (length s1) s2 = s1.
@@ -203,7 +203,7 @@ Qed.
 
 (** Test if, starting at position [n], [s1] occurs in [s2]; if
     so it returns the position *)
- 
+
 Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
   match s2, n with
   | EmptyString, 0 =>
@@ -212,7 +212,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
       | String a s1' => None
       end
   | EmptyString, S n' => None
-  | String b s2', 0 => 
+  | String b s2', 0 =>
       if prefix s1 s2 then Some 0
       else
         match index 0 s1 s2' with
@@ -230,7 +230,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
 Opaque prefix.
 
 (** If the result of [index] is [Some m], [s1] in [s2] at position [m] *)
- 
+
 Theorem index_correct1 :
  forall (n m : nat) (s1 s2 : string),
  index n s1 s2 = Some m -> substring m (length s1) s2 = s1.
@@ -260,9 +260,9 @@ intros x H H1; apply H; injection H1; intros H2; injection H2; auto.
 intros; discriminate.
 Qed.
 
-(** If the result of [index] is [Some m], 
+(** If the result of [index] is [Some m],
     [s1] does not occur in [s2] before [m] *)
- 
+
 Theorem index_correct2 :
  forall (n m : nat) (s1 s2 : string),
  index n s1 s2 = Some m ->
@@ -305,9 +305,9 @@ apply Lt.lt_S_n; auto.
 intros; discriminate.
 Qed.
 
-(** If the result of [index] is [None], [s1] does not occur in [s2] 
+(** If the result of [index] is [None], [s1] does not occur in [s2]
     after [n] *)
- 
+
 Theorem index_correct3 :
  forall (n m : nat) (s1 s2 : string),
  index n s1 s2 = None ->
@@ -349,7 +349,7 @@ Transparent prefix.
 
 (** If we are searching for the [Empty] string and the answer is no
     this means that [n] is greater than the size of [s] *)
- 
+
 Theorem index_correct4 :
  forall (n : nat) (s : string),
  index n EmptyString s = None -> length s < n.
@@ -368,7 +368,7 @@ Qed.
 
 (** Same as [index] but with no optional type, we return [0] when it
     does not occur *)
- 
+
 Definition findex n s1 s2 :=
   match index n s1 s2 with
   | Some n => n