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

7 files changed, 20 insertions, 20 deletions

diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
index da612c4367..e3dbd127f9 100644
--- a/plugins/subtac/test/ListDep.v
+++ b/plugins/subtac/test/ListDep.v
@@ -22,7 +22,7 @@ Section Map_DependentRecursor.
   Variable l : list U.
   Variable f : { x : U | In x l } -> V.
 
-  Obligations Tactic := unfold sub_list in * ; 
+  Obligations Tactic := unfold sub_list in * ;
     program_simpl ; intuition.
 
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
@@ -32,16 +32,16 @@ Section Map_DependentRecursor.
       | cons x tl => let tl' := map_rec tl in
 	f x :: tl'
     end.
-    
+
   Next Obligation.
     destruct_call map_rec.
     simpl in *.
     subst l'.
     simpl ; auto with arith.
   Qed.
-      
+
   Program Definition map : list V := map_rec l.
-    
+
 End Map_DependentRecursor.
 
 Extraction map.
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
index 05fc0803fc..2cea0841de 100644
--- a/plugins/subtac/test/ListsTest.v
+++ b/plugins/subtac/test/ListsTest.v
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Section Accessors.
   Variable A : Set.
 
-  Program Definition myhd : forall (l : list A | length l <> 0), A :=  
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=
     fun l =>
       match l with
         | nil => !
@@ -34,22 +34,22 @@ Section app.
     match l with
       | nil => l'
       | hd :: tl => hd :: (tl ++ l')
-    end 
+    end
     where "x ++ y" := (app x y).
 
   Next Obligation.
     intros.
     destruct_call app ; program_simpl.
   Defined.
-  
+
   Program Lemma app_id_l : forall l : list A, l = nil ++ l.
   Proof.
     simpl ; auto.
   Qed.
-  
+
   Program Lemma app_id_r : forall l : list A, l = l ++ nil.
   Proof.
-    induction l ; simpl in * ; auto. 
+    induction l ; simpl in * ; auto.
     rewrite <- IHl ; auto.
   Qed.
 
@@ -61,7 +61,7 @@ Section Nth.
 
   Variable A : Set.
 
-  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := 
+  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
     match n, l with
       | 0, hd :: _ => hd
       | S n', _ :: tl => nth tl n'
@@ -70,7 +70,7 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    simpl in *. auto with arith. 
+    simpl in *. auto with arith.
   Defined.
 
   Next Obligation.
@@ -78,7 +78,7 @@ Section Nth.
     inversion H.
   Qed.
 
-  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
+  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
     match l, n with
       | hd :: _, 0 => hd
       | _ :: tl, S n' => nth' tl n'
@@ -86,7 +86,7 @@ Section Nth.
     end.
   Next Obligation.
   Proof.
-    simpl in *. auto with arith. 
+    simpl in *. auto with arith.
   Defined.
 
   Next Obligation.
diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
index ac49ca96a4..01e2d75f33 100644
--- a/plugins/subtac/test/Mutind.v
+++ b/plugins/subtac/test/Mutind.v
@@ -1,11 +1,11 @@
 Require Import List.
 
-Program Fixpoint f a : { x : nat | x > 0 } := 
+Program Fixpoint f a : { x : nat | x > 0 } :=
   match a with
   | 0 => 1
   | S a' => g a a'
   end
-with g a b : { x : nat | x > 0 } := 
+with g a b : { x : nat | x > 0 } :=
   match b with
   | 0 => 1
   | S b' => f b'
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
index 14b8085496..7e0755d571 100644
--- a/plugins/subtac/test/Test1.v
+++ b/plugins/subtac/test/Test1.v
@@ -1,4 +1,4 @@
-Program Definition test (a b : nat) : { x : nat | x = a + b } := 
+Program Definition test (a b : nat) : { x : nat | x = a + b } :=
   ((a + b) : { x : nat | x = a + b }).
 Proof.
 intros.
diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
index 501aa79815..97c3d9414d 100644
--- a/plugins/subtac/test/euclid.v
+++ b/plugins/subtac/test/euclid.v
@@ -1,12 +1,12 @@
 Require Import Coq.Program.Program.
 Require Import Coq.Arith.Compare_dec.
 Notation "( x & y )" := (existS _ x y) : core_scope.
-  
+
 Require Import Omega.
 
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in
   (S q' & r)
   else (O & a).
 
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
index 2e17959c3e..90ae8bae84 100644
--- a/plugins/subtac/test/take.v
+++ b/plugins/subtac/test/take.v
@@ -11,7 +11,7 @@ Print cons.
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
   | 0 => nil
-  | S p => 
+  | S p =>
     match l with
     | cons hd tl => let rest := take tl p in cons hd rest
     | nil => !
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v
index 49fec2b80c..5ccc154afd 100644
--- a/plugins/subtac/test/wf.v
+++ b/plugins/subtac/test/wf.v
@@ -29,7 +29,7 @@ Require Import Wf_nat.
 
 Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
   { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in
   (S q' & r)
   else (O & a).
 destruct b ; simpl_subtac.