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

3 files changed, 39 insertions, 39 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index dcb10f3cf..bc42c6564 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -39,7 +39,7 @@ Qed.
 Hint Resolve diff_true_false : bool v62.
 
 Lemma diff_false_true : false <> true.
-Proof. 
+Proof.
   red in |- *; intros H; apply diff_true_false.
   symmetry  in |- *.
 assumption.
@@ -129,7 +129,7 @@ Qed.
 (************************)
 (** * A synonym of [if] on [bool] *)
 (************************)
- 
+
 Definition ifb (b1 b2 b3:bool) : bool :=
   match b1 with
     | true => b2
@@ -186,7 +186,7 @@ Proof.
   trivial with bool.
   trivial with bool.
 Qed.
- 
+
 Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false.
 Proof.
   destruct b.
@@ -318,7 +318,7 @@ Hint Resolve orb_comm orb_assoc: bool v62.
 (** * Properties of [andb]     *)
 (*******************************)
 
-Lemma andb_true_iff : 
+Lemma andb_true_iff :
   forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true.
 Proof.
  destruct b1; destruct b2; intuition.
@@ -382,7 +382,7 @@ Hint Resolve andb_false_elim: bool v62.
 Lemma andb_negb_r : forall b:bool, b && negb b = false.
 Proof.
   destruct b; reflexivity.
-Qed.   
+Qed.
 Hint Resolve andb_negb_r: bool v62.
 
 Notation andb_neg_b := andb_negb_r (only parsing).
@@ -542,8 +542,8 @@ Qed.
 
 (** Lemmas about the [b = true] embedding of [bool] to [Prop] *)
 
-Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. 
-Proof. 
+Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2.
+Proof.
   intros b1 b2; case b1; case b2; intuition.
 Qed.
 
@@ -556,7 +556,7 @@ Qed.
 
 Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *)
 
-Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.  
+Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.
 Proof.
   destruct b; intuition.
 Qed.
@@ -628,7 +628,7 @@ Qed.
 
 (** [Is_true] and connectives *)
 
-Lemma orb_prop_elim : 
+Lemma orb_prop_elim :
   forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
 Proof.
   destruct a; destruct b; simpl; tauto.
@@ -636,7 +636,7 @@ Qed.
 
 Notation orb_prop2 := orb_prop_elim (only parsing).
 
-Lemma orb_prop_intro : 
+Lemma orb_prop_intro :
   forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b).
 Proof.
   destruct a; destruct b; simpl; tauto.
@@ -663,16 +663,16 @@ Hint Resolve andb_prop_elim: bool v62.
 
 Notation andb_prop2 := andb_prop_elim (only parsing).
 
-Lemma eq_bool_prop_intro : 
-  forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. 
-Proof. 
+Lemma eq_bool_prop_intro :
+  forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2.
+Proof.
   destruct b1; destruct b2; simpl in *; intuition.
 Qed.
 
 Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2).
-Proof. 
+Proof.
   intros b1 b2; case b1; case b2; intuition.
-Qed. 
+Qed.
 
 Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b.
 Proof.
@@ -696,26 +696,26 @@ Qed.
 
 (** Rewrite rules about andb, orb and if (used in romega) *)
 
-Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), 
-  (if b && b' then a else a') = 
+Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool),
+  (if b && b' then a else a') =
   (if b then if b' then a else a' else a').
 Proof.
  destruct b; destruct b'; auto.
 Qed.
 
-Lemma negb_if : forall (A:Type)(a a':A)(b:bool), 
- (if negb b then a else a') = 
+Lemma negb_if : forall (A:Type)(a a':A)(b:bool),
+ (if negb b then a else a') =
  (if b then a' else a).
 Proof.
  destruct b; auto.
 Qed.
 
 (*****************************************)
-(** * Alternative versions of [andb] and [orb] 
+(** * Alternative versions of [andb] and [orb]
     with lazy behavior (for vm_compute)  *)
 (*****************************************)
 
-Notation "a &&& b" := (if a then b else false) 
+Notation "a &&& b" := (if a then b else false)
  (at level 40, left associativity) : lazy_bool_scope.
 Notation "a ||| b" := (if a then true else b)
  (at level 50, left associativity) : lazy_bool_scope.
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 9dbd90f05..2682a8848 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -16,7 +16,7 @@ Require Import Arith.
 
 Open Local Scope nat_scope.
 
-(** 
+(**
 On s'inspire de List.v pour fabriquer les vecteurs de bits.
 La dimension du vecteur est un paramètre trop important pour
 se contenter de la fonction "length".
@@ -27,22 +27,22 @@ La seconde idée est de faire un type dépendant dans lequel la
 longueur est un paramètre de construction. Cela complique un
 peu les inductions structurelles et dans certains cas on
 utilisera un terme de preuve comme définition, car le
-mécanisme d'inférence du type du filtrage n'est pas toujours 
+mécanisme d'inférence du type du filtrage n'est pas toujours
 aussi puissant que celui implanté par les tactiques d'élimination.
 *)
 
 Section VECTORS.
 
-(** 
+(**
 Un vecteur est une liste de taille n d'éléments d'un ensemble A.
-Si la taille est non nulle, on peut extraire la première composante et 
-le reste du vecteur, la dernière composante ou rajouter ou enlever 
+Si la taille est non nulle, on peut extraire la première composante et
+le reste du vecteur, la dernière composante ou rajouter ou enlever
 une composante (carry) ou repeter la dernière composante en fin de vecteur.
 On peut aussi tronquer le vecteur de ses p dernières composantes ou
 au contraire l'étendre (concaténer) d'un vecteur de longueur p.
 Une fonction unaire sur A génère une fonction des vecteurs de taille n
 dans les vecteurs de taille n en appliquant f terme à terme.
-Une fonction binaire sur A génère une fonction des couples de vecteurs 
+Une fonction binaire sur A génère une fonction des couples de vecteurs
 de taille n dans les vecteurs de taille n en appliquant f terme à terme.
 *)
 
@@ -93,7 +93,7 @@ Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
 Proof.
   induction n as [| n f]; intros a v.
   exact (Vcons a 0 v).
-  
+
   inversion v as [| a0 n0 H0 H1 ].
   exact (Vcons a (S n) (f a H0)).
 Defined.
@@ -103,7 +103,7 @@ Proof.
   induction n as [| n f]; intro v.
   inversion v.
   exact (Vcons a 1 v).
-  
+
   inversion v as [| a n0 H0 H1 ].
   exact (Vcons a (S (S n)) (f H0)).
 Defined.
@@ -113,9 +113,9 @@ Proof.
   induction p as [| p f]; intros H v.
   rewrite <- minus_n_O.
   exact v.
-  
+
   apply (Vshiftout (n - S p)).
-  
+
   rewrite minus_Sn_m.
   apply f.
   auto with *.
@@ -147,7 +147,7 @@ Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 Proof.
   induction n as [| n h]; intros v v0.
   exact Vnil.
-  
+
   inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
   exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
@@ -180,7 +180,7 @@ Qed.
 
 End VECTORS.
 
-(* suppressed: incompatible with Coq-Art book 
+(* suppressed: incompatible with Coq-Art book
 Implicit Arguments Vnil [A].
 Implicit Arguments Vcons [A n].
 *)
@@ -188,12 +188,12 @@ Implicit Arguments Vcons [A n].
 Section BOOLEAN_VECTORS.
 
 (**
-Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. 
+Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe.
 ATTENTION : le stockage s'effectue poids FAIBLE en tête.
 On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
 On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
 On calcule les décalages d'une position vers la gauche (vers les poids forts, on
-utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en 
+utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en
 insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
 ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
 (ils ne travaillent que sur des vecteurs au moins de longueur un).
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 03aa8baeb..06ab77cfb 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -39,18 +39,18 @@ Defined.
 Section connectives.
 
   Variables A B C D : Prop.
-  
+
   Hypothesis H1 : {A} + {B}.
   Hypothesis H2 : {C} + {D}.
-  
+
   Definition sumbool_and : {A /\ C} + {B \/ D}.
     case H1; case H2; auto.
   Defined.
-  
+
   Definition sumbool_or : {A \/ C} + {B /\ D}.
     case H1; case H2; auto.
   Defined.
-  
+
   Definition sumbool_not : {B} + {A}.
     case H1; auto.
   Defined.