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

4 files changed, 27 insertions, 27 deletions

diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
index 746e7c9976..d4a39296a0 100644
--- a/plugins/field/LegacyField_Compl.v
+++ b/plugins/field/LegacyField_Compl.v
@@ -13,7 +13,7 @@ Require Import List.
 Definition assoc_2nd :=
   (fix assoc_2nd_rec (A:Type) (B:Set)
                      (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
-                     (lst:list (prod A B)) {struct lst} : 
+                     (lst:list (prod A B)) {struct lst} :
    B -> A -> A :=
      fun (key:B) (default:A) =>
        match lst with
@@ -26,7 +26,7 @@ Definition assoc_2nd :=
        end).
 
 Definition mem :=
-  (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) 
+  (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2})
            (a:A) (l:list A) {struct l} : bool :=
      match l with
      | nil => false
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
index 63d9bdda69..5c1f228ac6 100644
--- a/plugins/field/LegacyField_Tactic.v
+++ b/plugins/field/LegacyField_Tactic.v
@@ -29,17 +29,17 @@ Ltac mem_assoc var lvar :=
       end
   end.
 
-Ltac number lvar := 
+Ltac number lvar :=
   let rec number_aux lvar cpt :=
     match constr:lvar with
     | (@nil ?X1) => constr:(@nil (prod X1 nat))
     | ?X2 :: ?X3 =>
         let l2 := number_aux X3 (S cpt) in
-        constr:((X2,cpt) :: l2) 
+        constr:((X2,cpt) :: l2)
     end
   in number_aux lvar 0.
 
-Ltac build_varlist FT trm := 
+Ltac build_varlist FT trm :=
   let rec seek_var lvar trm :=
     let AT := get_component A FT
     with AzeroT := get_component Azero FT
@@ -244,11 +244,11 @@ Ltac inverse_test FT :=
 
 Ltac apply_simplif sfun :=
   match goal with
-  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) => 
+  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) =>
   sfun X1 X2 X3
   end;
    match goal with
-   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) => 
+   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) =>
    sfun X1 X2 X3
    end.
 
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index 131ba84b83..378efa0353 100644
--- a/plugins/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
@@ -13,7 +13,7 @@ Require Import Peano_dec.
 Require Import LegacyRing.
 Require Import LegacyField_Compl.
 
-Record Field_Theory : Type := 
+Record Field_Theory : Type :=
   {A : Type;
    Aplus : A -> A -> A;
    Amult : A -> A -> A;
@@ -59,7 +59,7 @@ Proof.
   right; red in |- *; intro; inversion H1; auto.
   elim (eq_nat_dec n n0); intro y.
   left; rewrite y; auto.
-  right; red in |- *; intro; inversion H; auto. 
+  right; red in |- *; intro; inversion H; auto.
 Defined.
 
 Definition eq_nat_dec := Eval compute in eq_nat_dec.
@@ -149,7 +149,7 @@ Proof.
   repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
   legacy ring.
 Qed.
- 
+
 Lemma r_AmultT_mult :
  forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2.
 Proof.
@@ -164,22 +164,22 @@ Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
 Proof.
   intro; legacy ring.
 Qed.
- 
+
 Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
 Proof.
   intro; legacy ring.
 Qed.
- 
+
 Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
 Proof.
   intro; legacy ring.
 Qed.
- 
+
 Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
 Proof.
   intros; rewrite AmultT_comm; apply Th_inv_defT; auto.
 Qed.
- 
+
 Lemma Rmult_neq_0_reg :
  forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
 Proof.
@@ -298,7 +298,7 @@ Lemma assoc_mult_correct1 :
 Proof.
 simple induction e1; auto; intros.
 rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
- simpl in |- *; rewrite merge_mult_correct; simpl in |- *; 
+ simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
  auto.
 Qed.
 
@@ -318,7 +318,7 @@ simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
  rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1;
  fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
  rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
- rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; 
+ rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc;
  legacy ring.
 simpl in |- *; rewrite (H0 lvar); auto.
 simpl in |- *; rewrite (H0 lvar); auto.
@@ -365,7 +365,7 @@ Lemma assoc_plus_correct :
 Proof.
 simple induction e1; auto; intros.
 rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
- simpl in |- *; rewrite merge_plus_correct; simpl in |- *; 
+ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
  auto.
 Qed.
 
@@ -388,7 +388,7 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
         (interp_ExprA lvar e1))); rewrite <- AplusT_assoc;
  rewrite
   (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
-  ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *; 
+  ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *;
  rewrite (H0 lvar);
  rewrite <-
   (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1))
@@ -402,13 +402,13 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
   (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
      (interp_ExprA lvar e1)); apply AplusT_comm.
 unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
- fold interp_ExprA in |- *; rewrite assoc_mult_correct; 
+ fold interp_ExprA in |- *; rewrite assoc_mult_correct;
  rewrite (H0 lvar); simpl in |- *; auto.
 simpl in |- *; rewrite (H0 lvar); auto.
 simpl in |- *; rewrite (H0 lvar); auto.
 simpl in |- *; rewrite (H0 lvar); auto.
 unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
- fold interp_ExprA in |- *; rewrite assoc_mult_correct; 
+ fold interp_ExprA in |- *; rewrite assoc_mult_correct;
  simpl in |- *; auto.
 Qed.
 
@@ -466,7 +466,7 @@ Proof.
 simple induction e1; try intros; simpl in |- *.
 rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *;
  apply AmultT_Or.
-rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. 
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
 rewrite AmultT_comm;
  rewrite
   (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
@@ -629,7 +629,7 @@ Lemma monom_simplif_correct :
 Proof.
 simple induction e; intros; auto.
 simpl in |- *; case (eqExprA a e0); intros.
-rewrite <- e2; apply monom_simplif_rem_correct; auto. 
+rewrite <- e2; apply monom_simplif_rem_correct; auto.
 simpl in |- *; trivial.
 Qed.
 
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 7401491e45..2b4651dfb9 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -44,12 +44,12 @@ let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
 
 let lookup env typ =
   try Gmap.find typ !th_tab
-  with Not_found -> 
+  with Not_found ->
     errorlabstrm "field"
       (str "No field is declared for type" ++ spc() ++
       Printer.pr_lconstr_env env typ)
 
-let _ = 
+let _ =
   let init () = th_tab := Gmap.empty in
   let freeze () = !th_tab in
   let unfreeze fs = th_tab := fs in
@@ -116,7 +116,7 @@ END
 
 (* For the translator, otherwise the code above is OK *)
 open Ppconstr
-let pp_minus_div_arg _prc _prlc _prt (omin,odiv) = 
+let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
   if omin=None && odiv=None then mt() else
     spc() ++ str "with" ++
     pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
@@ -128,7 +128,7 @@ let () =
     (globwit_minus_div_arg,pp_minus_div_arg)
     (wit_minus_div_arg,pp_minus_div_arg)
 *)
-ARGUMENT EXTEND minus_div_arg 
+ARGUMENT EXTEND minus_div_arg
   TYPED AS constr_opt * constr_opt
   PRINTED BY pp_minus_div_arg
 | [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
@@ -137,7 +137,7 @@ ARGUMENT EXTEND minus_div_arg
 END
 
 VERNAC COMMAND EXTEND Field
-  [ "Add" "Legacy" "Field" 
+  [ "Add" "Legacy" "Field"
       constr(a) constr(aplus) constr(amult) constr(aone)
       constr(azero) constr(aopp) constr(aeq)
       constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]