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

6 files changed, 201 insertions, 201 deletions

diff --git a/plugins/groebner/GroebnerR.v b/plugins/groebner/GroebnerR.v
index 9122540d7..fc01c5886 100644
--- a/plugins/groebner/GroebnerR.v
+++ b/plugins/groebner/GroebnerR.v
@@ -6,15 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* 
+(*
  Tactic groebnerR: proofs of polynomials equalities with variables in R.
  Use Hilbert Nullstellensatz and Buchberger algorithm (adapted version of
  L.Thery Coq proven implementation).
  Thanks to B.Gregoire and L.Thery for help on ring tactic.
  Examples at the end of the file.
- 
+
  3 versions:
- 
+
  - groebnerR.
 
  - groebnerRp (a::b::c::nil) : give the list of variables are considered as
@@ -41,7 +41,7 @@ Declare ML Module "groebner_plugin".
 Local Open Scope R_scope.
 
 Lemma psos_r1b: forall x y, x - y = 0 -> x = y.
-intros x y H; replace x with ((x - y) + y);  
+intros x y H; replace x with ((x - y) + y);
   [rewrite H | idtac]; ring.
 Qed.
 
@@ -71,8 +71,8 @@ auto.
 Qed.
 
 
-Ltac equalities_to_goal := 
-  lazymatch goal with 
+Ltac equalities_to_goal :=
+  lazymatch goal with
   |  H: (@eq R ?x 0) |- _ => try revert H
   |  H: (@eq R 0 ?x) |- _ =>
           try generalize (sym_equal H); clear H
@@ -93,17 +93,17 @@ Qed.
 
 (* Removes x<>0 from hypothesis *)
 Ltac groebnerR_not_hyp:=
- match goal with 
+ match goal with
  | H: ?x<>?y |- _ =>
   match y with
-   |0 => 
+   |0 =>
      let H1:=fresh "Hgroebner" in
      let y:=fresh "x" in
      destruct (@groebnerR_not1_0 _ H) as (y,H1); clear H
    |_ => generalize (@groebnerR_diff _ _ H); clear H; intro
   end
  end.
- 
+
 Ltac groebnerR_not_goal :=
  match goal with
  | |- ?x<>?y :> R => red; intro; apply groebnerR_not2
@@ -124,10 +124,10 @@ Definition PEZ := PExpr Z.
 
 Definition P0Z : PolZ := @P0 Z 0%Z.
 
-Definition PolZadd : PolZ -> PolZ -> PolZ := 
+Definition PolZadd : PolZ -> PolZ -> PolZ :=
   @Padd Z 0%Z Zplus Zeq_bool.
 
-Definition PolZmul : PolZ -> PolZ -> PolZ := 
+Definition PolZmul : PolZ -> PolZ -> PolZ :=
   @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool.
 
 Definition PolZeq := @Peq Z Zeq_bool.
@@ -143,7 +143,7 @@ Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ :=
 
 Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) :=
  match lla with
- | List.nil => lp 
+ | List.nil => lp
  | la::lla => compute_list lla ((mult_l la lp)::lp)
  end.
 
@@ -154,10 +154,10 @@ Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
 
 
 (* Correction *)
-Definition PhiR : list R -> PolZ -> R := 
+Definition PhiR : list R -> PolZ -> R :=
   (Pphi 0 Rplus Rmult (gen_phiZ 0 1 Rplus Rmult Ropp)).
 
-Definition PEevalR : list R -> PEZ -> R := 
+Definition PEevalR : list R -> PEZ -> R :=
    PEeval 0 Rplus Rmult Rminus Ropp (gen_phiZ 0 1 Rplus Rmult Ropp)
          Nnat.nat_of_N pow.
 
@@ -188,20 +188,20 @@ Proof.
 Qed.
 
 Lemma PolZeq_correct : forall P P' l,
-  PolZeq P P' = true -> 
+  PolZeq P P' = true ->
   PhiR l P = PhiR l P'.
 Proof.
- intros;apply 
+ intros;apply
    (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (F_R Rfield)));trivial.
 Qed.
 
 Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
-  match l with 
+  match l with
   | List.nil => True
   | a::l => Interp a = 0 /\ Cond0 A Interp l
   end.
 
-Lemma mult_l_correct : forall l la lp, 
+Lemma mult_l_correct : forall l la lp,
   Cond0 PolZ (PhiR l) lp ->
   PhiR l (mult_l la lp) = 0.
 Proof.
@@ -220,7 +220,7 @@ Proof.
  apply mult_l_correct;trivial.
 Qed.
 
-Lemma check_correct : 
+Lemma check_correct :
   forall l lpe qe certif,
     check lpe qe certif = true ->
     Cond0 PEZ (PEevalR l) lpe ->
@@ -228,11 +228,11 @@ Lemma check_correct :
 Proof.
  unfold check;intros l lpe qe (lla, lq) H2 H1.
  apply PolZeq_correct with (l:=l) in H2.
- rewrite norm_correct, H2. 
+ rewrite norm_correct, H2.
  apply mult_l_correct.
  apply compute_list_correct.
  clear H2 lq lla qe;induction lpe;simpl;trivial.
- simpl in H1;destruct H1. 
+ simpl in H1;destruct H1.
  rewrite <- norm_correct;auto.
 Qed.
 
@@ -244,7 +244,7 @@ elim (Rmult_integral _ _ H0);intros.
  absurd (c=0);auto.
 
  clear H0; induction r; simpl in *.
-  contradict H1; discrR. 
+  contradict H1; discrR.
 
   elim (Rmult_integral _ _ H1); auto.
 Qed.
@@ -255,10 +255,10 @@ Ltac generalise_eq_hyps:=
     (match goal with
      |h : (?p = ?q)|- _ => revert h
      end).
-  
+
 Ltac lpol_goal t :=
   match t with
-  | ?a = 0 -> ?b => 
+  | ?a = 0 -> ?b =>
     let r:= lpol_goal b in
     constr:(a::r)
   | ?a = 0 => constr:(a::nil)
@@ -274,25 +274,25 @@ Fixpoint IPR p {struct p}: R :=
   end.
 
 Definition IZR1 z :=
-  match z with Z0 => 0 
-             | Zpos p => IPR p 
-             | Zneg p => -(IPR p) 
+  match z with Z0 => 0
+             | Zpos p => IPR p
+             | Zneg p => -(IPR p)
   end.
 
 Fixpoint interpret3 t fv {struct t}: R :=
   match t with
-  | (PEadd t1 t2) => 
+  | (PEadd t1 t2) =>
        let v1  := interpret3 t1 fv in
        let v2  := interpret3 t2 fv in (v1 + v2)
-  | (PEmul t1 t2) => 
+  | (PEmul t1 t2) =>
        let v1  := interpret3 t1 fv in
        let v2  := interpret3 t2 fv in (v1 * v2)
-  | (PEsub t1 t2) => 
+  | (PEsub t1 t2) =>
        let v1  := interpret3 t1 fv in
        let v2  := interpret3 t2 fv in (v1 - v2)
-  | (PEopp t1) => 
+  | (PEopp t1) =>
        let v1  := interpret3 t1 fv in (-v1)
-  | (PEpow t1 t2) => 
+  | (PEpow t1 t2) =>
        let v1  := interpret3 t1 fv in v1 ^(Nnat.nat_of_N t2)
   | (PEc t1) => (IZR1 t1)
   | (PEX n) => List.nth (pred (nat_of_P n)) fv 0
@@ -303,7 +303,7 @@ Fixpoint interpret3 t fv {struct t}: R :=
 Ltac parametres_en_tete fv lp :=
     match fv with
      | (@nil _)          => lp
-     | (@cons _ ?x ?fv1) => 
+     | (@cons _ ?x ?fv1) =>
        let res := AddFvTail x lp in
          parametres_en_tete fv1 res
     end.
@@ -340,7 +340,7 @@ Ltac groebner_call nparam p lp kont :=
         groebner_call_n nparam p n lp kont ||
         let n' := eval compute in (Nsucc n) in try_n n'
     end in
-  try_n 1%N. 
+  try_n 1%N.
 
 
 Ltac groebnerR_gen lparam lvar n RNG lH _rl :=
@@ -351,7 +351,7 @@ Ltac groebnerR_gen lparam lvar n RNG lH _rl :=
   let t := Get_goal in
   let lpol := lpol_goal t in
   intros;
-  let fv := 
+  let fv :=
     match lvar with
     | nil =>
         let fv1 := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
@@ -381,7 +381,7 @@ Ltac groebnerR_gen lparam lvar n RNG lH _rl :=
     set (lp21:=lp);
     groebner_call nparam p lp ltac:(fun c r lq lci =>
       set (q := PEmul c (PEpow p21 r));
-      let Hg := fresh "Hg" in 
+      let Hg := fresh "Hg" in
       assert (Hg:check lp21 q (lci,lq) = true);
       [ (vm_compute;reflexivity) || idtac "invalid groebner certificate"
       | let Hg2 := fresh "Hg" in
diff --git a/plugins/groebner/GroebnerZ.v b/plugins/groebner/GroebnerZ.v
index 8fd14aee2..7c40bbb70 100644
--- a/plugins/groebner/GroebnerZ.v
+++ b/plugins/groebner/GroebnerZ.v
@@ -26,7 +26,7 @@ intros x y H. contradict H. f_equal. assumption.
 Qed.
 
 Ltac groebnerZversR1 :=
- repeat 
+ repeat
   (match goal with
    | H:(@eq Z ?x ?y) |- _ =>
        generalize (@groebnerZhypR _ _ H); clear H; intro H
@@ -68,6 +68,6 @@ Ltac groebnerZ_begin :=
  simpl in *.
  (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*)
 
-Ltac groebnerZ := 
+Ltac groebnerZ :=
  groebnerZ_begin; (*idtac "groebnerZ_begin;";*)
  groebnerR.
diff --git a/plugins/groebner/groebner.ml4 b/plugins/groebner/groebner.ml4
index da41a89b6..cc1b08a63 100644
--- a/plugins/groebner/groebner.ml4
+++ b/plugins/groebner/groebner.ml4
@@ -75,17 +75,17 @@ module BigInt = struct
   let hash x =
     try (int_of_big_int x)
     with _-> 1
-  let puis = power_big_int_positive_int 
+  let puis = power_big_int_positive_int
 
   (* a et b positifs, résultat positif *)
-  let rec pgcd a b = 
-    if equal b coef0 
+  let rec pgcd a b =
+    if equal b coef0
     then a
     else if lt a b then pgcd b a else pgcd b (modulo a b)
 
 
   (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
-  let pgcd2 a b = 
+  let pgcd2 a b =
     if equal a coef0 then b
     else if equal b coef0 then a
     else let c = pgcd (abs a) (abs b) in
@@ -113,7 +113,7 @@ module Ent = struct
   let coef0 = Entiers.ent0
   let coef1 = Entiers.ent1
   let to_string = Entiers.string_of_ent
-  let to_int x = Entiers.int_of_ent x 
+  let to_int x = Entiers.int_of_ent x
   let hash x =Entiers.hash_ent x
   let signe = Entiers.signe_ent
 
@@ -122,14 +122,14 @@ module Ent = struct
     |_ -> (mult p (puis p (n-1)))
 
   (* a et b positifs, résultat positif *)
-  let rec pgcd a b = 
-    if equal b coef0 
+  let rec pgcd a b =
+    if equal b coef0
     then a
     else if lt a b then pgcd b a else pgcd b (modulo a b)
 
 
   (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
-  let pgcd2 a b = 
+  let pgcd2 a b =
     if equal a coef0 then b
     else if equal b coef0 then a
     else let c = pgcd (abs a) (abs b) in
@@ -175,7 +175,7 @@ let tpexpr =
   lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
 let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
 let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX")
-let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd")  
+let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd")
 let ttsub = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEsub")
 let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul")
 let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp")
@@ -202,7 +202,7 @@ let mkt_app name l =  mkApp (Lazy.force name, Array.of_list l)
 let tlp () = mkt_app tlist [mkt_app tpexpr [Lazy.force tz]]
 let tllp () = mkt_app tlist [tlp()]
 
-let rec mkt_pos n = 
+let rec mkt_pos n =
   if n =/ num_1 then Lazy.force pxH
   else if mod_num n num_2 =/ num_0 then
     mkt_app pxO [mkt_pos (quo_num n num_2)]
@@ -214,7 +214,7 @@ let mkt_n n =
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
-let mkt_z z  = 
+let mkt_z z  =
   if z =/ num_0 then  Lazy.force z0
   else if z >/ num_0 then
     mkt_app zpos [mkt_pos z]
@@ -224,14 +224,14 @@ let mkt_z z  =
 let rec mkt_term t  =  match t with
 | Zero -> mkt_term (Const num_0)
 | Const r -> let (n,d) = numdom r in
-  mkt_app  ttconst [Lazy.force tz; mkt_z n]     
-| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)]     
+  mkt_app  ttconst [Lazy.force tz; mkt_z n]
+| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)]
 | Opp t1 -> mkt_app  ttopp [Lazy.force tz; mkt_term t1]
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
-| Pow (t1,n) ->  if (n = 0) then 
-    mkt_app ttconst [Lazy.force tz; mkt_z num_1]     
+| Pow (t1,n) ->  if (n = 0) then
+    mkt_app ttconst [Lazy.force tz; mkt_z num_1]
 else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
 
@@ -270,10 +270,10 @@ let rec parse_term p =
     else Zero
 | _ -> Zero
 
-let rec parse_request lp = 
+let rec parse_request lp =
   match kind_of_term lp with
     | App (_,[|_|])  -> []
-    | App (_,[|_;p;lp1|])  -> 
+    | App (_,[|_;p;lp1|])  ->
 	(parse_term p)::(parse_request lp1)
     |_-> assert false
 
@@ -433,7 +433,7 @@ let rec remove_list_tail l i =
    ...
    [cn+m n+m-1,...,cn+m 1]]
 
-   enleve les polynomes intermediaires inutiles pour calculer le dernier 
+   enleve les polynomes intermediaires inutiles pour calculer le dernier
  *)
 
 let remove_zeros zero lci =
@@ -491,7 +491,7 @@ let theoremedeszeros_termes lp =
       for i=m downto 1 do lvar:=["x"^string_of_int i^""]@(!lvar); done;
       name_var:=!lvar;
 
-      let lp = List.map (term_pol_sparse nparam) lp in 
+      let lp = List.map (term_pol_sparse nparam) lp in
       match lp with
       | [] -> assert false
       | p::lp1 ->
@@ -499,7 +499,7 @@ let theoremedeszeros_termes lp =
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
 	  match remove_zeros (fun x -> x=zeroP) lc with
-	  | [] -> assert false 
+	  | [] -> assert false
 	  | (lq::lci) ->
 	      (* lci commence par les nouveaux polynomes *)
 	      let m= !nvars in
@@ -524,7 +524,7 @@ let groebner lpol =
   init_constants ();
   let lp= parse_request lpol in
   let (_lp0,_p,c,r,_lci,_lq as rthz) = theoremedeszeros_termes lp in
-  let certif = certificat_vers_polynome_creux rthz in 
+  let certif = certificat_vers_polynome_creux rthz in
   let certif = hash_certif certif in
   let certif = certif_term certif in
   let c = mkt_term c in
diff --git a/plugins/groebner/ideal.ml4 b/plugins/groebner/ideal.ml4
index 73db36d46..eae849921 100644
--- a/plugins/groebner/ideal.ml4
+++ b/plugins/groebner/ideal.ml4
@@ -9,15 +9,15 @@
 (*i camlp4deps: "lib/refutpat.cmo" i*)
 (* NB: The above camlp4 extension adds a let* syntax for refutable patterns *)
 
-(* 
+(*
    Nullstellensatz par calcul de base de Grobner
 
    On utilise une representation creuse des polynomes:
-   un monome est un tableau d'exposants (un par variable), 
+   un monome est un tableau d'exposants (un par variable),
    avec son degre en tete.
    un polynome est une liste de (coefficient,monome).
 
-   L'algorithme de Buchberger a proprement parler est tire du code caml 
+   L'algorithme de Buchberger a proprement parler est tire du code caml
    extrait du code Coq ecrit par L.Thery.
 
  *)
@@ -250,10 +250,10 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
       | e -> s:= (!s) @ [((getvar !lvar (i-1)) ^ "^" ^ e)]);
     done;
     (match !s with
-      [] -> if coefone 
+      [] -> if coefone
       then  "1"
       else ""
-    | l -> if coefone 
+    | l -> if coefone
     then  (String.concat "*" l)
     else ( "*" ^
            (String.concat "*" l)))
@@ -267,22 +267,22 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
   | "-1" ->( "-" ^" "^(string_of_mon m true))
   | c -> if (String.get c 0)='-'
   then ( "- "^
-         (String.sub c 1 
+         (String.sub c 1
             ((String.length c)-1))^
          (string_of_mon m false))
   else (match start with
     true -> ( c^(string_of_mon m false))
   |false -> ( "+ "^
               c^(string_of_mon m false)))
-  and stringP p start = 
+  and stringP p start =
     if (zeroP p)
-    then (if start 
+    then (if start
     then ("0")
     else "")
     else ((string_of_term (hdP p) start)^
           " "^
           (stringP (tlP p) false))
-  in 
+  in
   (stringP p true)
 
 
@@ -299,12 +299,12 @@ let print_pol zeroP hdP tlP coefterm monterm string_of_coef
       | e -> s:= (!s) @ [((getvar !lvar (i-1)) ^ "^" ^ e)]);
     done;
     (match !s with
-      [] -> if coefone 
+      [] -> if coefone
       then print_string "1"
       else ()
-    | l -> if coefone 
+    | l -> if coefone
     then print_string (String.concat "*" l)
-    else (print_string "*"; 
+    else (print_string "*";
           print_string (String.concat "*" l)))
   and print_term t start = let a = coefterm t and m = monterm t in
   match (string_of_coef a) with
@@ -316,16 +316,16 @@ let print_pol zeroP hdP tlP coefterm monterm string_of_coef
   | "-1" ->(print_string "-";print_space();print_mon m true)
   | c -> if (String.get c 0)='-'
   then (print_string "- ";
-        print_string (String.sub c 1 
+        print_string (String.sub c 1
                         ((String.length c)-1));
         print_mon m false)
   else (match start with
     true -> (print_string c;print_mon m false)
   |false -> (print_string "+ ";
              print_string c;print_mon m false))
-  and printP p start = 
+  and printP p start =
     if (zeroP p)
-    then (if start 
+    then (if start
     then print_string("0")
     else ())
     else (print_term (hdP p) start;
@@ -340,7 +340,7 @@ let print_pol zeroP hdP tlP coefterm monterm string_of_coef
 
 let name_var= ref []
 
-let stringP = string_of_pol 
+let stringP = string_of_pol
     (fun p -> match p with [] -> true | _ -> false)
     (fun p -> match p with (t::p) -> t |_ -> failwith "print_pol dans dansideal")
     (fun p -> match p with (t::p) -> p |_ -> failwith "print_pol dans dansideal")
@@ -362,7 +362,7 @@ let rec lstringP l =
     [] -> ""
   |p::l -> (stringP p)^("\n")^(lstringP l)
 
-let printP = print_pol 
+let printP = print_pol
     (fun p -> match p with [] -> true | _ -> false)
     (fun p -> match p with (t::p) -> t |_ -> failwith "print_pol dans dansideal")
     (fun p -> match p with (t::p) -> p |_ -> failwith "print_pol dans dansideal")
@@ -388,17 +388,17 @@ let zeroP = []
 (* Retourne un polynome constant à d variables *)
 let polconst d c =
   let m = Array.create (d+1) 0 in
-  let m = set_deg d m in 
+  let m = set_deg d m in
   [(c,m)]
 
 
-    
+
 (* somme de polynomes= liste de couples (int,monomes) *)
 let plusP d p q =
   let rec plusP p q =
     match p with
       [] -> q
-    |t::p' -> 
+    |t::p' ->
 	match q with
 	  [] -> p
 	|t'::q' ->
@@ -434,7 +434,7 @@ let rec selectdiv d m l =
 let gen d i =
   let m = Array.create (d+1) 0 in
   m.(i) <- 1;
-  let m = set_deg d m in 
+  let m = set_deg d m in
   [(coef1,m)]
 
 
@@ -503,13 +503,13 @@ let add_hmon m q =
   if !use_hmon then Hashtbl.add hmon m q
 
 let selectdiv_cache d m l =
-  try find_hmon m 
-  with Not_found -> 
+  try find_hmon m
+  with Not_found ->
     match selectdiv d m l with
 	[] -> []
       | q -> add_hmon m q; q
 
-let div_pol d p q a b m = 
+let div_pol d p q a b m =
 (*  info ".";*)
   plusP d (emultP a p) (mult_t_pol d b m q)
 
@@ -532,7 +532,7 @@ let reduce2 d p l =
 	    let (c,r)=(reduce p') in
             (c,((P.multP a c,m)::r))
 	  else (coef1,p)
-      |(b,m')::q' -> 
+      |(b,m')::q' ->
           let c=(pgcdpos a b) in
           let a'= (P.divP b c) in
           let b'=(P.oppP (P.divP a c)) in
@@ -544,7 +544,7 @@ let reduce2 d p l =
 (* trace des divisions *)
 
 (* liste des polynomes de depart *)
-let poldep = ref [] 
+let poldep = ref []
 let poldepcontent = ref []
 
 
@@ -552,7 +552,7 @@ module HashPolPair = Hashtbl.Make
   (struct
      type t = poly * poly
      let equal (p,q) (p',q') = equal p p' && equal q q'
-     let hash (p,q) = 
+     let hash (p,q) =
        let c = List.map fst p @ List.map fst q in
        let m = List.map snd p @ List.map snd q in
        List.fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c
@@ -576,7 +576,7 @@ let initcoefpoldep d lp =
     (fun p -> coefpoldep_set p p (polconst d coef1))
     lp
 
-(* garde la trace dans coefpoldep 
+(* garde la trace dans coefpoldep
    divise sans pseudodivisions *)
 
 let reduce2_trace d p l lcp =
@@ -586,10 +586,10 @@ let reduce2_trace d p l lcp =
       [] -> ([],[])
     |t::p' -> let (a,m)=t in
       let q =
-	(try Hashtbl.find hmon m 
-	with Not_found -> 
+	(try Hashtbl.find hmon m
+	with Not_found ->
 	  let q = selectdiv d m l in
-	  match q with 
+	  match q with
             t'::q' -> (Hashtbl.add hmon m q;q)
           |[] -> q) in
       match q with
@@ -599,7 +599,7 @@ let reduce2_trace d p l lcp =
 	    let (lq,r)=(reduce p') in
             (lq,((a,m)::r))
 	  else ([],p)
-      |(b,m')::q' -> 
+      |(b,m')::q' ->
           let b' = P.oppP (P.divP a b) in
           let m''= div_mon d m m' in
           let p1=plusP d p' (mult_t_pol d b' m'' q') in
@@ -627,7 +627,7 @@ let reduce2_trace d p l lcp =
        c)
      lcp
      !poldep,
-   r)     
+   r)
 
 (***********************************************************************
   Algorithme de Janet (V.P.Gerdt Involutive algorithms...)
@@ -640,7 +640,7 @@ let homogeneous = ref false
 let pol_courant = ref []
 
 
-type pol3 = 
+type pol3 =
    {pol : poly;
     anc : poly;
     nmp : mon}
@@ -697,7 +697,7 @@ let monom_multiplicative d u s =
     then m.(i)<- 1;
   done;
   m
-    
+
 (* mu monome des variables multiplicative de u *)
 let janet_div_mon d u mu v =
   let res = ref true in
@@ -709,7 +709,7 @@ let janet_div_mon d u mu v =
     i:= !i + 1;
   done;
   !res
-    
+
 let find_multiplicative p mg =
   try Hashpol.find mg p.pol
   with Not_found -> (info "\nPROBLEME DANS LA TABLE DES VAR MULT";
@@ -727,7 +727,7 @@ let find_reductor d v lt mt =
     let r =
       List.find
 	(fun q ->
-	  let u = fst_mon q in 
+	  let u = fst_mon q in
 	  let mu =  find_multiplicative q mt in
 	  janet_div_mon d u mu v
 	)
@@ -793,11 +793,11 @@ let criteria d p g lt =
 
 let head_normal_form d p lt mt =
   let h = ref (p.pol) in
-  let res = 
+  let res =
   try (
     let v = snd(List.hd !h) in
     let g = ref (find_reductor d v lt mt) in
-    if snd(List.hd !h) <> lm_anc p && criteria d p !g lt 
+    if snd(List.hd !h) <> lm_anc p && criteria d p !g lt
     then ((* info "=";*) [])
     else (
       while !h <> [] && (!g).pol <> [] do
@@ -848,14 +848,14 @@ let head_reduce d lq lt mt =
   (*info ("temps de head_reduce: "
 	^(Format.sprintf "@[%10.3f@]s\n" ((Unix.gettimeofday ())-.t1)));*)
   !lq
-  
+
 let choose_irreductible d lf =
   List.hd lf
 (* bien plus lent
     (List.sort (fun p q -> compare_mon d (fst_mon p.pol) (fst_mon q.pol)) lf)
 *)
-    
-    
+
+
 let hashtbl_multiplicative d lf =
   let mg = Hashpol.create 51 in
   hashtbl_reductor := Hashtbl.create 51;
@@ -867,10 +867,10 @@ let hashtbl_multiplicative d lf =
   (*info ("temps de hashtbl_multiplicative: "
 	^(Format.sprintf "@[%10.3f@]s\n" ((Unix.gettimeofday ())-.t1)));*)
   mg
-    
+
 let list_diff l x =
   List.filter (fun y -> y <> x) l
-    
+
 let janet2 d lf p0 =
   hashtbl_reductor := Hashtbl.create 51;
   let t1 = Unix.gettimeofday() in
@@ -889,14 +889,14 @@ let janet2 d lf p0 =
   while !lq <> [] && !r <> [] do
     let p = choose_irreductible d !lq in
     lq := list_diff !lq p;
-    if p.pol = p.anc 
+    if p.pol = p.anc
     then ( (* on enleve de lt les pol divisibles par p et on les met dans lq *)
       let m = fst_mon p in
       let lt1 = !lt in
       List.iter
-	(fun q -> 
+	(fun q ->
 	  let m'= fst_mon q in
-	  if div_strict d m m' 
+	  if div_strict d m m'
 	  then (
 	    lq := (!lq) @ [q];
 	    lt := list_diff !lt q))
@@ -916,13 +916,13 @@ let janet2 d lf p0 =
       if !r <> []
       then (
 	List.iter
-	  (fun q -> 
+	  (fun q ->
 	    let mq = find_multiplicative q !mt in
 	    for i=1 to d do
 	      if mq.(i) = 1
 	      then q.nmp.(i)<- 0
 	      else
-		if q.nmp.(i) = 0 
+		if q.nmp.(i) = 0
 		then (
 		  (* info "+";*)
 		  lq := (!lq) @
@@ -945,17 +945,17 @@ let janet2 d lf p0 =
   info ("--- fin Janet2\n");
   info ("temps: "^(Format.sprintf "@[%10.3f@]s\n" ((Unix.gettimeofday ())-.t1)));
   List. map (fun q -> q.pol) !lt
-   
+
 (**********************************************************************
  version 3 *)
 
 let head_normal_form3 d p lt mt =
   let h = ref (p.pol) in
-  let res = 
+  let res =
   try (
     let v = snd(List.hd !h) in
     let g = ref (find_reductor d v lt mt) in
-    if snd(List.hd !h) <> lm_anc p && criteria d p !g lt  
+    if snd(List.hd !h) <> lm_anc p && criteria d p !g lt
     then ((* info "=";*) [])
     else (
       while !h <> [] && (!g).pol <> [] do
@@ -979,7 +979,7 @@ let head_normal_form3 d p lt mt =
 	^(Format.sprintf "@[%10.3f@]s\n" ((Unix.gettimeofday ())-.t1)));*)
   res
 
-    
+
 let janet3 d lf p0 =
   hashtbl_reductor := Hashtbl.create 51;
   let t1 = Unix.gettimeofday() in
@@ -997,14 +997,14 @@ let janet3 d lf p0 =
     let* p::lq1 = !lq in
     lq := lq1;
 (*
-    if p.pol = p.anc 
+    if p.pol = p.anc
     then ( (* on enleve de lt les pol divisibles par p et on les met dans lq *)
       let m = fst_mon (p.pol) in
       let lt1 = !lt in
       List.iter
-	(fun q -> 
+	(fun q ->
 	  let m'= fst_mon (q.pol) in
-	  if div_strict d m m' 
+	  if div_strict d m m'
 	  then (
 	    lq := (!lq) @ [q];
 	    lt := list_diff !lt q))
@@ -1040,7 +1040,7 @@ let janet3 d lf p0 =
 	      if mq.(i) = 1
 	      then q.nmp.(i)<- 0
 	      else
-		if q.nmp.(i) = 0 
+		if q.nmp.(i) = 0
 		then (
 		  (* info "+";*)
 		  lq := (!lq) @
@@ -1116,7 +1116,7 @@ let etrangers d p p'=
   !res
 
 
-(* teste si le monome dominant de p'' 
+(* teste si le monome dominant de p''
    divise le ppcm des monomes dominants de p et p' *)
 
 let div_ppcm d p p' p'' =
@@ -1150,10 +1150,10 @@ let rec slice d i a = function
       else addRes b (slice d i a q1)
 
 let rec addS x l = l @[x]
-			  
+
 let addSugar x l =
   if !sugar_flag
-  then 
+  then
     let sx = sugar x in
     let rec insere l  =
       match l with
@@ -1165,13 +1165,13 @@ let addSugar x l =
     in insere l
   else addS x l
 
-(* ajoute les spolynomes de i avec la liste de polynomes aP, 
+(* ajoute les spolynomes de i avec la liste de polynomes aP,
    a la liste q *)
 
 let rec genPcPf d i aP q =
   match aP with
       [] -> q
-    | a::l1 -> 
+    | a::l1 ->
         (match slice d i a l1 with
              Keep l2 -> addSugar (spol d i a) (genPcPf d i l2 q)
            | DontKeep l2 -> genPcPf d i l2 q)
@@ -1183,7 +1183,7 @@ let rec genOCPf d = function
 let step = ref 0
 
 let infobuch p q =
-  if !step = 0 
+  if !step = 0
   then (info ("[" ^ (string_of_int (List.length p))
               ^ "," ^  (string_of_int (List.length q))
               ^ "]"))
@@ -1266,8 +1266,8 @@ let pbuchf d pq p lp0=
   info "calcul de la base de Groebner\n";
   step:=0;
   Hashtbl.clear hmon;
-  let rec pbuchf lp lpc = 
-      infobuch lp lpc; 
+  let rec pbuchf lp lpc =
+      infobuch lp lpc;
 (*      step:=(!step+1)mod 10;*)
       match lpc with
         [] -> test_dans_ideal d p lp lp0
@@ -1297,7 +1297,7 @@ let pbuchf d pq p lp0=
 		poldepcontent:=addS ct (!poldepcontent);
 		try test_dans_ideal d p (addS a0 lp) lp0
 		with NotInIdeal -> pbuchf (addS a0 lp) (genPcPf d a0 lp lpc2)
-  in pbuchf (fst pq) (snd pq) 
+  in pbuchf (fst pq) (snd pq)
 
 let is_homogeneous p =
   match p with
@@ -1315,8 +1315,8 @@ let is_homogeneous p =
    [a(n+m,n+m-1);...;a(n+m,1)]]
    lc = [qn+m; ... q1]
 
-   tels que 
-   c*p = sum qi*pi 
+   tels que
+   c*p = sum qi*pi
    ou pn+k = a(n+k,n+k-1)*pn+k-1 + ... + a(n+k,1)* p1
  *)
 
diff --git a/plugins/groebner/polynom.ml b/plugins/groebner/polynom.ml
index 6d2ed26e8..0a9c3e270 100644
--- a/plugins/groebner/polynom.ml
+++ b/plugins/groebner/polynom.ml
@@ -127,17 +127,17 @@ end
 module Make (C:Coef) = struct
 
 type coef = C.t
-let coef_of_int i = C.of_num (Num.Int i) 
+let coef_of_int i = C.of_num (Num.Int i)
 let coef0 = coef_of_int 0
 let coef1 = coef_of_int 1
 
 type variable = int
 
-type t = 
+type t =
     Pint of coef                    (* polynome constant *)
   | Prec of variable * (t array)    (* coefficients par degre croissant *)
 
-(* sauf mention du contraire, les opérations ne concernent que des 
+(* sauf mention du contraire, les opérations ne concernent que des
    polynomes normalisés:
    - les variables sont des entiers strictement positifs.
    - les coefficients d'un polynome en x ne font intervenir que des variables < x.
@@ -149,12 +149,12 @@ type t =
 let of_num x = Pint (C.of_num x)
 let cf0 = of_num (Num.Int 0)
 let cf1 = of_num (Num.Int 1)
-	    
+
 (* la n-ième variable *)
 let x n = Prec (n,[|cf0;cf1|])
 
 (* crée rapidement v^n *)
-let monome v n = 
+let monome v n =
   match n with
       0->Pint coef1;
     |_->let tmp = Array.create (n+1) (Pint coef0) in
@@ -169,7 +169,7 @@ let is_constantP = function
 
 
 (* conversion d'un poly cst en entier*)
-let int_of_Pint = function 
+let int_of_Pint = function
     Pint x -> x
   | _ -> failwith "non"
 
@@ -179,15 +179,15 @@ let is_zero p =
   match p with Pint n -> if C.equal n coef0 then true else false |_-> false
 
 (* variable max *)
-let max_var_pol p = 
-  match p with 
+let max_var_pol p =
+  match p with
       Pint _ -> 0
     |Prec(x,_) -> x
 
 
 (* p n'est pas forcément normalisé *)
 let rec max_var_pol2 p =
-  match p with 
+  match p with
       Pint _ -> 0
     |Prec(v,c)-> Array.fold_right (fun q m -> max (max_var_pol2 q) m) c v
 
@@ -196,11 +196,11 @@ let rec max_var_pol2 p =
 let rec max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 
-(* Egalité de deux polynômes 
+(* Egalité de deux polynômes
    On ne peut pas utiliser = car elle ne marche pas sur les Big_int.
 *)
 let rec equal p q =
-  match (p,q) with 
+  match (p,q) with
       (Pint a,Pint b) -> C.equal a b
     |(Prec(x,p1),Prec(y,q1)) ->
        if x<>y then false
@@ -216,17 +216,17 @@ let rec equal p q =
    sont supposés normalisés.
    si constant, rend le coef constant.
 *)
-	
+
 let rec norm p = match p with
     Pint _ -> p
   |Prec (x,a)->
      let d = (Array.length a -1) in
-     let n = ref d in 
+     let n = ref d in
        while !n>0 && (equal a.(!n) (Pint coef0)) do
 	 n:=!n-1;
        done;
        if !n<0 then Pint coef0
-       else if !n=0 then a.(0) 
+       else if !n=0 then a.(0)
        else if !n=d then p
        else (let b=Array.create (!n+1) (Pint coef0) in
                for i=0 to !n do b.(i)<-a.(i);done;
@@ -235,14 +235,14 @@ let rec norm p = match p with
 
 (* degré en la variable v du polynome p, v >= max var de p *)
 let rec deg v p =
-  match p with 
+  match p with
       Prec(x,p1) when x=v -> Array.length p1 -1
     |_ -> 0
 
 
 (* degré total *)
 let rec deg_total p =
-  match p with 
+  match p with
       Prec (x,p1) -> let d = ref 0 in
         Array.iteri (fun i q -> d:= (max !d (i+(deg_total q)))) p1;
         !d
@@ -258,7 +258,7 @@ let rec copyP p =
 
 (* coefficient de degre i en v, v >= max var de p *)
 let coef v i p =
-  match p with 
+  match p with
       Prec (x,p1) when x=v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
     |_ -> if i=0 then p else Pint coef0
 
@@ -273,20 +273,20 @@ let rec plusP p q =
        |(Prec (x,p1),Pint b) -> let p2=Array.map copyP p1 in
            p2.(0)<- plusP p1.(0) q;
            Prec (x,p2)
-       |(Prec (x,p1),Prec (y,q1)) -> 
+       |(Prec (x,p1),Prec (y,q1)) ->
           if x<y then (let q2=Array.map copyP q1 in
                          q2.(0)<- plusP p q1.(0);
                          Prec (y,q2))
           else if x>y then (let p2=Array.map copyP p1 in
                               p2.(0)<- plusP p1.(0) q;
                               Prec (x,p2))
-          else 
-            (let n=max (deg x p) (deg x q) in 
+          else
+            (let n=max (deg x p) (deg x q) in
              let r=Array.create (n+1) (Pint coef0) in
                for i=0 to n do
                  r.(i)<- plusP (coef x i p) (coef x i q);
                done;
-               Prec(x,r))) 
+               Prec(x,r)))
   in norm res
 
 
@@ -324,8 +324,8 @@ let rec multx n v p =
           p2.(i+n)<-p1.(i);
         done;
         Prec (x,p2)
-    |_ -> if p = (Pint coef0) then (Pint coef0) 
-       else (let p2=Array.create (n+1) (Pint coef0) in 
+    |_ -> if p = (Pint coef0) then (Pint coef0)
+       else (let p2=Array.create (n+1) (Pint coef0) in
                p2.(n)<-p;
                Prec (v,p2))
 
@@ -338,13 +338,13 @@ let rec multP p q =
        if C.equal a coef0 then Pint coef0
        else let q2 = Array.map (fun z-> multP p z) q1 in
          Prec (y,q2)
-           
+
     |(Prec (x,p1), Pint b) ->
        if C.equal b coef0 then Pint coef0
        else let p2 = Array.map (fun z-> multP z q) p1 in
          Prec (x,p2)
     |(Prec (x,p1), Prec(y,q1)) ->
-       if x<y 
+       if x<y
        then (let q2 = Array.map (fun z-> multP p z) q1 in
                Prec (y,q2))
        else if x>y
@@ -357,7 +357,7 @@ let rec multP p q =
 
 (* derive p par rapport a la variable v, v >= max_var p *)
 let rec deriv v p =
-  match p with 
+  match p with
       Pint a -> Pint coef0
     | Prec(x,p1) when x=v ->
        let d = Array.length p1 -1 in
@@ -373,7 +373,7 @@ let rec deriv v p =
 
 (* opposé de p *)
 let rec oppP p =
-  match p with 
+  match p with
       Pint a -> Pint (C.opp a)
     |Prec(x,p1) -> Prec(x,Array.map oppP p1)
 
@@ -428,7 +428,7 @@ let rec coef_constant p =
   match p with
       Pint a->a
     |Prec(_,q)->coef_constant q.(0)
-       
+
 
 (***********************************************************************
   3. Affichage des polynômes.
@@ -437,13 +437,13 @@ let rec coef_constant p =
 (* si univ=false, on utilise x,y,z,a,b,c,d... comme noms de variables,
    sinon, x1,x2,...
 *)
-let univ=ref true 
+let univ=ref true
 
 (* joli jusqu'a trois variables -- sinon changer le 'w' *)
 let string_of_var x=
   if !univ then
     "u"^(string_of_int x)
-  else 
+  else
     if x<=3 then String.make 1 (Char.chr(x+(Char.code 'w')))
     else String.make 1 (Char.chr(x-4+(Char.code 'a')))
 
@@ -452,8 +452,8 @@ let nsP = ref 0
 let rec string_of_Pcut p =
   if (!nsP)<=0
   then "..."
-  else 
-  match p with 
+  else
+  match p with
   |Pint a-> nsP:=(!nsP)-1;
       if C.le coef0 a
       then C.to_string a
@@ -467,7 +467,7 @@ let rec string_of_Pcut p =
       then s:=st0;
     let fin = ref false in
     for i=(Array.length t)-1 downto 1 do
-      if (!nsP)<0 
+      if (!nsP)<0
       then (sp:="...";
 	    if not (!fin) then s:=(!s)^"+"^(!sp);
 	    fin:=true)
@@ -501,10 +501,10 @@ let rec string_of_Pcut p =
     if !s="" then (nsP:=(!nsP)-1;
 		   (s:="0"));
     !s
-      
+
 let to_string p =
   nsP:=20;
-  string_of_Pcut p 
+  string_of_Pcut p
 
 let printP p = Format.printf "@[%s@]" (to_string p)
 
@@ -526,13 +526,13 @@ let print_lpoly lp = print_tpoly (Array.of_list lp)
 (* rend (s,r) tel que p = s*q+r *)
 let rec quo_rem_pol p q x =
   if x=0
-  then (match (p,q) with 
+  then (match (p,q) with
           |(Pint a, Pint b) ->
-	     if C.equal (C.modulo a b) coef0 
+	     if C.equal (C.modulo a b) coef0
              then (Pint (C.div a b), cf0)
              else failwith "div_pol1"
 	  |_ -> assert false)
-  else 
+  else
     let m = deg x q in
     let b = coefDom x q in
     let q1 = remP x q in (* q = b*x^m+q1 *)
@@ -567,13 +567,13 @@ and div_pol p q x =
 		   )
 
 
-(* test de division exacte  de p par q mais constantes rationnels 
+(* test de division exacte  de p par q mais constantes rationnels
    à vérifier *)
 let divP p q=
   let x = max (max_var_pol p) (max_var_pol q) in
   div_pol p q x
 
-(* test de division exacte  de p par q mais constantes rationnels 
+(* test de division exacte  de p par q mais constantes rationnels
    à vérifier *)
 let div_pol_rat p q=
   let x = max (max_var_pol p) (max_var_pol q) in
@@ -600,7 +600,7 @@ let pseudo_div p q x =
   match q with
       Pint _ -> (cf0, q,1, p)
     | Prec (v,q1) when x<>v -> (cf0, q,1, p)
-    | Prec (v,q1) -> 
+    | Prec (v,q1) ->
 	(
 	  (*  pr "pseudo_division: c^d*p = s*q + r";*)
 	  let delta = ref 0 in
@@ -636,7 +636,7 @@ let rec pgcdP p q =
 and pgcd_pol p q x =
   pgcd_pol_rec p q x
 
-and content_pol p x = 
+and content_pol p x =
   match p with
       Prec(v,p1) when v=x ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) cf0 p1
@@ -647,8 +647,8 @@ and pgcd_coef_pol c p x =
       Prec(v,p1) when x=v ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) c  p1
     |_ -> pgcd_pol_rec c p (x-1)
-    
-  
+
+
 and pgcd_pol_rec p q x =
  match (p,q) with
 	(Pint a,Pint b) -> Pint (C.pgcd (C.abs a) (C.abs b))
@@ -686,7 +686,7 @@ and pgcd_pol_rec p q x =
    ai = (- ci+1)^(di + 1)
    b1 = 1
    bi = ci*si^di  si i>1
-   
+
    s1 = 1
    si+1 = ((ci+1)^di*si)/si^di
 
@@ -694,7 +694,7 @@ and pgcd_pol_rec p q x =
 and gcd_sub_res p q x =
   if equal q cf0
   then p
-  else 
+  else
     let d = deg x p in
     let d' = deg x q in
       if d<d'
@@ -704,9 +704,9 @@ and gcd_sub_res p q x =
 	let c' = coefDom x q in
 	let r = snd (quo_rem_pol (((oppP c')^^(delta+1))@@p) (oppP q) x) in
 	  gcd_sub_res_rec q r (c'^^delta) c' d' x
-	    
+
 and gcd_sub_res_rec p q s c d x =
-  if equal q cf0 
+  if equal q cf0
   then p
   else (
     let d' = deg x q in
@@ -731,7 +731,7 @@ and lazard_power c s d x =
 *)
 
 (*
-  p = f1 f2^2 ... fn^r 
+  p = f1 f2^2 ... fn^r
   p/\p'= f2 f3^2...fn^(r-1)
   sans_carré(p)= p/p/\p '= f1 f2 ... fn
 *)
@@ -815,9 +815,9 @@ let prfactorise () =
 		  print_lpoly (List.flatten c))
     hfactorise
 
-let factorise = 
-  memoP "f" hfactorise 
-    (fun p -> 
+let factorise =
+  memoP "f" hfactorise
+    (fun p ->
        let rec fact p x =
          if x=0
          then []
@@ -859,8 +859,8 @@ let set_of_array_facteurs tf =
 
 
 (* Factorise un tableau de polynômes f, et rend:
-   - un tableau p de facteurs (degré>0, contenu entier 1, 
-   coefficient de tête >0) obtenu par décomposition sans carrés 
+   - un tableau p de facteurs (degré>0, contenu entier 1,
+   coefficient de tête >0) obtenu par décomposition sans carrés
    puis par division mutuelle
    - un tableau l de couples (constante, listes d'indices l)
    tels que f.(i) = l.(i)_1*Produit(p.(j), j dans l.(i)_2)
@@ -887,7 +887,7 @@ let factorise_tableauP2 f l1 =
                     f l1 in
 	  pr ">";
 	  res
-	    
+
 let factorise_tableauP f =
   factorise_tableauP2 f (Array.map facteurs2 f)
 
@@ -901,9 +901,9 @@ let factorise_tableauP f =
 let rec is_positif p =
 
   let res =
-    match p with 
+    match p with
 	Pint a -> C.le coef0 a
-      |Prec(x,p1) -> 
+      |Prec(x,p1) ->
          (array_for_all is_positif p1)
 	 && (try (Array.iteri (fun i c -> if (i mod 2)<>0 && not (equal c cf0)
                                then failwith "pas pair")
@@ -919,7 +919,7 @@ let is_negatif p = is_positif (oppP p)
 
 
 (* rend r tel que deg r < deg q et r a le signe de p en les racines de q.
-   le coefficient dominant de q est non nul 
+   le coefficient dominant de q est non nul
    quand les polynômes de coef_non_nuls le sont.
    (rs,cs,ds,ss,crs,lpos,lpol)= pseudo_euclide coef_non_nuls vect.(s-1) res.(s-1) v
 *)
@@ -943,7 +943,7 @@ let pseudo_euclide coef_non_nuls p q x =
       let r = if d mod 2 = 1 then c@@r else r in
       let s = if d mod 2 = 1 then c@@s else s in
       let d = if d mod 2 = 1 then d+1 else d in
-    
+
     (* on encore  c^d * p = s*q + r, mais d pair *)
     if equal r cf0
     then ((*pr "reste nul"; *) (r,c,d,s,cf1,[],[]))
@@ -960,7 +960,7 @@ let pseudo_euclide coef_non_nuls p q x =
                        let k = ref 0 in
 			 (try (while true do
  				 let rd = div_pol !r f x in
-				   (* verification de la division 
+				   (* verification de la division
 				      if not (equal cf0 ((!r)--(f@@rd)))
 				      then failwith "erreur dans la division";
 				   *)
@@ -972,7 +972,7 @@ let pseudo_euclide coef_non_nuls p q x =
 	 		 lf:=(f,!k)::(!lf)))
           coef_non_nuls;
 	(* il faut éventuellement remultiplier pour garder le signe de r *)
-	let lpos = ref [] in 
+	let lpos = ref [] in
 	let lpol = ref [] in
 	  List.iter (fun (f,k) ->
 		       if k>0
@@ -1006,7 +1006,7 @@ let pseudo_euclide coef_non_nuls p q x =
 	  *)
 	  (* lpos = liste de (f,k) ou f est non nul positif, et f^k divise r0
 	     lpol = liste de (f,k) ou f non nul, k est pair et f^k divise r0
-	     on c^d * p = s*q + r0 
+	     on c^d * p = s*q + r0
 	     avec d pair
 	     r0 = cr * r * PI_lpos f^k * PI_lpol g^k
 	     cr non nul positif
@@ -1016,14 +1016,14 @@ let pseudo_euclide coef_non_nuls p q x =
 
 
 (* teste si la non-nullité des polynômes de lp entraîne celle de p:
-   chacun des facteurs de la décomposition sans carrés de p 
+   chacun des facteurs de la décomposition sans carrés de p
    divise un des polynômes de lp (dans Q[x1...xn]) *)
 
 let implique_non_nul lp p =
   if equal p cf0 then false
   else(
     pr "[";
-    let lf = facteurs2 p in 
+    let lf = facteurs2 p in
     let r =(
       try (List.iter (fun f ->
 			if (try (List.iter (fun q ->
diff --git a/plugins/groebner/utile.ml b/plugins/groebner/utile.ml
index fc7de1e33..40644489b 100644
--- a/plugins/groebner/utile.ml
+++ b/plugins/groebner/utile.ml
@@ -21,7 +21,7 @@ let info s =
 (**********************************************************************
   Listes
 *)
-	
+
 (* appartenance à une liste , on donne l'égalité *)
 let rec list_mem_eq eq x l =
   match l with
@@ -32,13 +32,13 @@ let rec list_mem_eq eq x l =
 let set_of_list_eq eq l =
    let res = ref [] in
    List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
-   List.rev !res 
+   List.rev !res
 
 
 (***********************************************************************
  Un outil pour faire une mémo-fonction:
  fonction est la fonction(!)
- memoire est une référence au graphe déjà calculé 
+ memoire est une référence au graphe déjà calculé
     (liste de couples, c'est une variable globale)
  egal est l'égalité sur les arguments
  valeur est une valeur possible de la fonction (sert uniquement pour le typage)
@@ -56,9 +56,9 @@ let memo memoire egal valeur fonction x =
    with _ -> !res
 
 
-(* un autre plus efficace, 
+(* un autre plus efficace,
    utilisant une fonction intermediaire (utile si on n'a pas
-   l'égalité = sur les arguments de fonction) 
+   l'égalité = sur les arguments de fonction)
    s chaîne imprimée s'il n'y a pas calcul *)
 
 let memos s memoire print fonction x =
@@ -71,8 +71,8 @@ let memos s memoire print fonction x =
 
 (**********************************************************************
   Eléments minimaux pour un ordre partiel de division.
-  E est un ensemble, avec une multiplication 
-  et une division partielle div (la fonction div peut échouer), 
+  E est un ensemble, avec une multiplication
+  et une division partielle div (la fonction div peut échouer),
   constant est un prédicat qui définit un sous-ensemble C de E.
 *)
 (*
@@ -128,7 +128,7 @@ let factorise_tableau div zero c f l1 =
       let r = ref p in
       let li = ref [] in
       if not (zero p)
-      then 
+      then
       Array.iteri (fun j q ->
 	              try (while true do
                                let rr = div !r q in
@@ -140,12 +140,12 @@ let factorise_tableau div zero c f l1 =
       res.(i)<-(!r,!li))
      f;
     (l1,res)
-   
+
 
 (* exemples:
 
 let l =  [1;2;6;24;720]
-and div1 = (fun a b -> if a mod b =0 then a/b else failwith "div") 
+and div1 = (fun a b -> if a mod b =0 then a/b else failwith "div")
 and constant = (fun x -> x<2)
 and zero = (fun x -> x=0)