[coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

3 files changed, 243 insertions, 243 deletions

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 7ea56b41ec..46685e6a63 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -87,13 +87,13 @@ let compare_mon (m : mon) (m' : mon) =
      (* degre lexicographique inverse *)
     match Int.compare m.(0) m'.(0) with
     | 0 -> (* meme degre total *)
-	let res=ref 0 in
-	let i=ref d in
-	while (!res=0) && (!i>=1) do
-	  res:= - (Int.compare m.(!i) m'.(!i));
-	  i:=!i-1;
-	done;
-	!res
+        let res=ref 0 in
+        let i=ref d in
+        while (!res=0) && (!i>=1) do
+          res:= - (Int.compare m.(!i) m'.(!i));
+          i:=!i-1;
+        done;
+        !res
     | x -> x)
 
 let div_mon m m' =
@@ -135,13 +135,13 @@ let ppcm_mon m m' =
 (* returns a constant polynom ial with d variables *)
 let const_mon d =
   let m = Array.make (d+1) 0 in
-  let m = set_deg m in 
+  let m = set_deg m in
   m
 
 let var_mon d i =
   let m = Array.make (d+1) 0 in
   m.(i) <- 1;
-  let m = set_deg m in 
+  let m = set_deg m in
   m
 
 end
@@ -174,7 +174,7 @@ type polynom = {
 
 (**********************************************************************
   Polynomials
-  list of (coefficient, monomial) decreasing order 
+  list of (coefficient, monomial) decreasing order
 *)
 
 let repr p = p
@@ -216,10 +216,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)))
@@ -233,26 +233,26 @@ 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)
 
 let stringP metadata (p : poly) =
-  string_of_pol 
+  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")
@@ -309,7 +309,7 @@ let coef_of_int x = P.of_num (Num.Int x)
 
 (* variable i *)
 let gen d i =
-  let m = var_mon d i in 
+  let m = var_mon d i in
   [((coef_of_int 1),m)]
 
 let oppP p =
@@ -349,7 +349,7 @@ let puisP p n=
           let q = multP q q in
           if n mod 2 = 0 then q else multP p q
       in puisP p n
-	
+
 (***********************************************************************
    Division of polynomials
  *)
@@ -366,7 +366,7 @@ type table = {
 let pgcdpos a b  = P.pgcdP a b
 
 let polynom0 = { pol = []; num = 0 }
-   
+
 let ppol p = p.pol
 
 let lm p = snd (List.hd (ppol p))
@@ -390,7 +390,7 @@ let rec selectdiv m l =
       true -> q
     |false -> selectdiv m r
 
-let div_pol p q a b m = 
+let div_pol p q a b m =
   plusP (emultP a p) (mult_t_pol b m q)
 
 let find_hmon table m = match table.hmon with
@@ -424,15 +424,15 @@ let reduce2 table p l =
     match p with
       [] -> (coef1,[])
     |t::p' ->
-	let (a,m)=t in
+        let (a,m)=t in
       let q = selectdiv table m l in
       match q with
-	[] -> if reduire_les_queues
-	then
-	  let (c,r)=(reduce p') in
+        [] -> if reduire_les_queues
+        then
+          let (c,r)=(reduce p') in
           (c,((P.multP a c,m)::r))
-	else (coef1,p)
-      |(b,m')::q' -> 
+        else (coef1,p)
+      |(b,m')::q' ->
           let c=(pgcdpos a b) in
           let a'= (div_coef b c) in
           let b'=(P.oppP (div_coef a c)) in
@@ -450,7 +450,7 @@ let coefpoldep_find table p q =
 let coefpoldep_set table p q c =
   Hashtbl.add table.coefpoldep (p.num,q.num) c
 
-(* keeps trace in coefpoldep 
+(* keeps trace in coefpoldep
    divides without pseudodivisions *)
 
 let reduce2_trace table p l lcp =
@@ -461,16 +461,16 @@ let reduce2_trace table p l lcp =
     match p with
       [] -> ([],[])
     |t::p' ->
-	let (a,m)=t in
+        let (a,m)=t in
       let q = selectdiv table m l in
       match q with
-	[] ->
-	  if reduire_les_queues
-	  then
-	    let (lq,r)=(reduce p') in
+        [] ->
+          if reduire_les_queues
+          then
+            let (lq,r)=(reduce p') in
             (lq,((a,m)::r))
-	  else ([],p)
-      |(b,m')::q' -> 
+          else ([],p)
+      |(b,m')::q' ->
           let b'=(P.oppP (div_coef a b)) in
           let m''= div_mon m m' in
           let p1=plusP p' (mult_t_pol b' m'' q') in
@@ -480,18 +480,18 @@ let reduce2_trace table p l lcp =
   (List.map2
      (fun c0 q ->
        let c =
-	 List.fold_left
-	   (fun x (a,m,s) ->
-	     if equal s (ppol q)
-	     then
-	       plusP x (mult_t_pol a m (polconst (nvar m) (coef_of_int 1)))
-	     else x)
-	   c0
-	   lq in
+         List.fold_left
+           (fun x (a,m,s) ->
+             if equal s (ppol q)
+             then
+               plusP x (mult_t_pol a m (polconst (nvar m) (coef_of_int 1)))
+             else x)
+           c0
+           lq in
        c)
      lcp
      lp,
-   r)     
+   r)
 
 (***********************************************************************
    Completion
@@ -511,12 +511,12 @@ let spol0 ps qs=
   let m1 = div_mon m'' m in
   let m2 = div_mon m'' m' in
   let fsp p' q' =
-    plusP 
-      (mult_t_pol 
-	 (div_coef b c)
-	 m1 p')
-      (mult_t_pol 
-	 (P.oppP (div_coef a c))
+    plusP
+      (mult_t_pol
+         (div_coef b c)
+         m1 p')
+      (mult_t_pol
+         (P.oppP (div_coef a c))
          m2 q') in
   let sp = fsp p' q' in
   let p0 = fsp (polconst (nvar m) (coef_of_int 1)) [] in
@@ -564,7 +564,7 @@ end
 
 let ord i j =
   if i<j then (i,j) else (j,i)
-    
+
 let cpair p q accu =
   if etrangers (ppol p) (ppol q) then accu
   else Heap.add (ord p.num q.num, ppcm_mon (lm p) (lm q)) accu
@@ -582,14 +582,14 @@ let critere3 table ((i,j),m) lp lcp =
     (fun h ->
       h.num <> i && h.num <> j
         && (div_mon_test m (lm h))
-	&& (h.num < j
-	   || not (m = ppcm_mon 
-		   (lm (table.allpol.(i)))
-		   (lm h)))
-	&& (h.num < i
-	  || not (m = ppcm_mon 
-		   (lm (table.allpol.(j)))
-		   (lm h))))
+        && (h.num < j
+           || not (m = ppcm_mon
+                   (lm (table.allpol.(i)))
+                   (lm h)))
+        && (h.num < i
+          || not (m = ppcm_mon
+                   (lm (table.allpol.(j)))
+                   (lm h))))
     lp
 
 let infobuch p q =
@@ -668,18 +668,18 @@ let pbuchf table metadata cur_pb homogeneous (lp, lpc) p =
       infobuch lp lpc;
       match Heap.pop lpc with
       | None ->
-	  test_dans_ideal cur_pb table metadata p lp len0
+          test_dans_ideal cur_pb table metadata p lp len0
       | Some (((i, j), m), lpc2) ->
-	  if critere3 table ((i,j),m) lp lpc2
-	  then (sinfo "c"; pbuchf cur_pb (lp, lpc2))
-	  else    
-	    let (a0, p0, q0) = spol0 table.allpol.(i) table.allpol.(j) in
-	    if homogeneous && a0 <>[] && deg_hom a0 > deg_hom cur_pb.cur_poly
-	    then (sinfo "h"; pbuchf cur_pb (lp, lpc2))
-	    else
+          if critere3 table ((i,j),m) lp lpc2
+          then (sinfo "c"; pbuchf cur_pb (lp, lpc2))
+          else
+            let (a0, p0, q0) = spol0 table.allpol.(i) table.allpol.(j) in
+            if homogeneous && a0 <>[] && deg_hom a0 > deg_hom cur_pb.cur_poly
+            then (sinfo "h"; pbuchf cur_pb (lp, lpc2))
+            else
 (*	      let sa = a.sugar in*)
               match reduce2 table a0 lp with
-		_, [] -> sinfo "0";pbuchf cur_pb (lp, lpc2)
+                _, [] -> sinfo "0";pbuchf cur_pb (lp, lpc2)
               | ca, _ :: _ ->
 (*		info "pair reduced\n";*)
                   let map q =
@@ -692,22 +692,22 @@ let pbuchf table metadata cur_pb homogeneous (lp, lpc) p =
                   let (lca, a0) = reduce2_trace table (emultP ca a0) lp lcp in
 (*		info "paire re-reduced";*)
                   let a = new_allpol table a0 in
-		  List.iter2 (fun c q -> coefpoldep_set table a q c) lca lp;
-		  let a0 = a in
-		  info (fun () -> "new polynomial: "^(stringPcut metadata (ppol a0)));
+                  List.iter2 (fun c q -> coefpoldep_set table a q c) lca lp;
+                  let a0 = a in
+                  info (fun () -> "new polynomial: "^(stringPcut metadata (ppol a0)));
                   let nlp = addS a0 lp in
-		  try test_dans_ideal cur_pb table metadata p nlp len0
-		  with NotInIdealUpdate cur_pb ->
-		    let newlpc = cpairs1 a0 lp lpc2 in
-		    pbuchf cur_pb (nlp, newlpc)
+                  try test_dans_ideal cur_pb table metadata p nlp len0
+                  with NotInIdealUpdate cur_pb ->
+                    let newlpc = cpairs1 a0 lp lpc2 in
+                    pbuchf cur_pb (nlp, newlpc)
   in pbuchf cur_pb (lp, lpc)
-    
+
 let is_homogeneous p =
   match p with
   | [] -> true
   | (a,m)::p1 -> let d = deg m in
     List.for_all (fun (b,m') -> deg m' =d) p1
-    
+
 (* returns
    c
    lp = [pn;...;p1]
@@ -719,7 +719,7 @@ let is_homogeneous p =
    lc = [qn+m; ... q1]
 
    such that
-   c*p = sum qi*pi 
+   c*p = sum qi*pi
    where pn+k = a(n+k,n+k-1)*pn+k-1 + ... + a(n+k,1)* p1
  *)
 
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 71a3132283..9ba83c0843 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -239,7 +239,7 @@ let rec parse_request lp =
   match Constr.kind lp with
     | App (_,[|_|])  -> []
     | App (_,[|_;p;lp1|])  ->
-	(parse_term p)::(parse_request lp1)
+        (parse_term p)::(parse_request lp1)
     |_-> assert false
 
 let set_nvars_term nvars t =
@@ -266,7 +266,7 @@ module Poly = Polynom.Make(Coef)
 module PIdeal = Ideal.Make(Poly)
 open PIdeal
 
-(* term to sparse polynomial 
+(* term to sparse polynomial
    variables <=np are in the coefficients
 *)
 
@@ -278,22 +278,22 @@ let term_pol_sparse nvars np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-	if Num.eq_num r num_0
-	then zeroP
-	else polconst d (Poly.Pint (Coef.of_num r))
+        if Num.eq_num r num_0
+        then zeroP
+        else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
-	let v = int_of_string v in
-	if v <= np
-	then polconst d (Poly.x v)
-	else gen d v
+        let v = int_of_string v in
+        if v <= np
+        then polconst d (Poly.x v)
+        else gen d v
     | Opp t1 ->  oppP (aux t1)
     | Add (t1,t2) -> plusP (aux t1) (aux t2)
     | Sub (t1,t2) -> plusP (aux t1) (oppP (aux t2))
     | Mul (t1,t2) -> multP (aux t1) (aux t2)
     | Pow (t1,n) ->  puisP (aux t1) n
-    in 
+    in
 (*       info ("donne: "^(stringP res)^"\n");*)
-       res 
+       res
   in
   let res= aux t in
   res
@@ -321,25 +321,25 @@ let pol_sparse_to_term n2 p =
       let m = Ideal.Monomial.repr m in
       let n = (Array.length m)-1 in
       let (i0,e0) =
-	List.fold_left (fun (r,d) (a,m) ->
+        List.fold_left (fun (r,d) (a,m) ->
               let m = Ideal.Monomial.repr m in
-	      let i0= ref 0 in
-	      for k=1 to n do
-		if m.(k)>0
-		then i0:=k
-	      done;
-	      if Int.equal !i0 0
-	      then (r,d)
-	      else if !i0 > r
-	      then (!i0, m.(!i0))
-	      else if Int.equal !i0 r && m.(!i0)<d
-	      then (!i0, m.(!i0))
-	      else (r,d))
-	  (0,0)
-	  p in
+              let i0= ref 0 in
+              for k=1 to n do
+                if m.(k)>0
+                then i0:=k
+              done;
+              if Int.equal !i0 0
+              then (r,d)
+              else if !i0 > r
+              then (!i0, m.(!i0))
+              else if Int.equal !i0 r && m.(!i0)<d
+              then (!i0, m.(!i0))
+              else (r,d))
+          (0,0)
+          p in
       if Int.equal i0 0
       then
-	let mp = polrec_to_term a in
+        let mp = polrec_to_term a in
         if List.is_empty p1 then mp else add (mp, aux p1)
       else
         let fold (p1, p2) (a, m) =
@@ -352,11 +352,11 @@ let pol_sparse_to_term n2 p =
             (p1, (a, m) :: p2)
         in
         let (p1, p2) = List.fold_left fold ([], []) p in
-	let vm =
-	  if Int.equal e0 1
-	  then Var (string_of_int (i0))
-	  else pow (Var (string_of_int (i0)),e0) in
-	add (mul(vm, aux (List.rev p1)), aux (List.rev p2))
+        let vm =
+          if Int.equal e0 1
+          then Var (string_of_int (i0))
+          else pow (Var (string_of_int (i0)),e0) in
+        add (mul(vm, aux (List.rev p1)), aux (List.rev p2))
   in   (*info "-> pol_sparse_to_term\n";*)
   aux p
 
@@ -410,34 +410,34 @@ open Ideal
  *)
 let clean_pol lp =
   let t = Hashpol.create 12 in
-  let find p = try Hashpol.find t p 
-               with 
+  let find p = try Hashpol.find t p
+               with
                  Not_found -> Hashpol.add t p true; false in
   let rec aux lp =
     match lp with
     | [] -> [], []
-    | p :: lp1 -> 
+    | p :: lp1 ->
       let clp, lb = aux lp1 in
-      if equal p zeroP ||  find p then clp, true::lb 
+      if equal p zeroP ||  find p then clp, true::lb
        else
         (p :: clp, false::lb) in
      aux lp
 
-(* Expand the list of polynomials lp putting zeros where the list of 
-   booleans lb indicates there is a missing element 
+(* Expand the list of polynomials lp putting zeros where the list of
+   booleans lb indicates there is a missing element
    Warning:
    the expansion is relative to the end of the list in reversed order
    lp cannot have less elements than lb
 *)
 let expand_pol lb lp =
- let rec aux lb lp = 
+ let rec aux lb lp =
    match lb with
    | [] -> lp
    | true :: lb1 ->  zeroP :: aux lb1 lp
    | false :: lb1 ->
      match lp with
      [] -> assert false
-     | p :: lp1 -> p :: aux lb1 lp1 
+     | p :: lp1 -> p :: aux lb1 lp1
   in List.rev (aux lb (List.rev lp))
 
 let theoremedeszeros_termes lp =
@@ -446,21 +446,21 @@ let theoremedeszeros_termes lp =
   | Const (Int sugarparam)::Const (Int nparam)::lp ->
       ((match sugarparam with
       |0 -> sinfo "computation without sugar";
-	  lexico:=false;
+          lexico:=false;
       |1 -> sinfo "computation with sugar";
-	  lexico:=false;
+          lexico:=false;
       |2 -> sinfo "ordre lexico computation without sugar";
-	  lexico:=true;
+          lexico:=true;
       |3 -> sinfo "ordre lexico computation with sugar";
-	  lexico:=true;
+          lexico:=true;
       |4 -> sinfo "computation without sugar, division by pairs";
-	  lexico:=false;
+          lexico:=false;
       |5 -> sinfo "computation with sugar, division by pairs";
-	  lexico:=false;
+          lexico:=false;
       |6 -> sinfo "ordre lexico computation without sugar, division by pairs";
-	  lexico:=true;
+          lexico:=true;
       |7 -> sinfo "ordre lexico computation with sugar, division by pairs";
-	  lexico:=true;
+          lexico:=true;
       | _ -> user_err Pp.(str "nsatz: bad parameter")
        );
       let lvar = List.init nvars (fun i -> Printf.sprintf "x%i" (i + 1)) in
@@ -471,32 +471,32 @@ let theoremedeszeros_termes lp =
       match lp with
       | [] -> assert false
       | p::lp1 ->
-	  let lpol = List.rev lp1 in
+          let lpol = List.rev lp1 in
           (* preprocessing :
              we remove zero polynomials and duplicate that are not handled by in_ideal
-             lb is kept in order to fix the certificate in the post-processing 
+             lb is kept in order to fix the certificate in the post-processing
           *)
-	  let lpol, lb  = clean_pol lpol in
-	  let cert = theoremedeszeros metadata nvars lpol p in
+          let lpol, lb  = clean_pol lpol in
+          let cert = theoremedeszeros metadata nvars lpol p in
           sinfo "cert ok";
-	  let lc = cert.last_comb::List.rev cert.gb_comb in
-	  match remove_zeros lc with
-	  | [] -> assert false
-	  | (lq::lci) ->
+          let lc = cert.last_comb::List.rev cert.gb_comb in
+          match remove_zeros lc with
+          | [] -> assert false
+          | (lq::lci) ->
               (* post-processing : we apply the correction for the last line *)
               let lq = expand_pol lb lq in
-	      (* lci commence par les nouveaux polynomes *)
-	      let m = nvars in
-	      let c = pol_sparse_to_term m (polconst m cert.coef) in
-	      let r = Pow(Zero,cert.power) in
-	      let lci = List.rev lci in
+              (* lci commence par les nouveaux polynomes *)
+              let m = nvars in
+              let c = pol_sparse_to_term m (polconst m cert.coef) in
+              let r = Pow(Zero,cert.power) in
+              let lci = List.rev lci in
               (* post-processing we apply the correction for the other lines *)
-	      let lci = List.map (expand_pol lb) lci in
-	      let lci = List.map (List.map (pol_sparse_to_term m)) lci in
-	      let lq = List.map (pol_sparse_to_term m) lq in
-	      info (fun () -> Printf.sprintf "number of parameters: %i" nparam);
-	      sinfo "term computed";
-	      (c,r,lci,lq)
+              let lci = List.map (expand_pol lb) lci in
+              let lci = List.map (List.map (pol_sparse_to_term m)) lci in
+              let lq = List.map (pol_sparse_to_term m) lq in
+              info (fun () -> Printf.sprintf "number of parameters: %i" nparam);
+              sinfo "term computed";
+              (c,r,lci,lq)
       )
   |_ -> assert false
 
@@ -526,13 +526,13 @@ let nsatz lpol =
   let res =
     List.fold_right
       (fun lt r ->
-	 let ltterm =
-	   List.fold_right
-	     (fun t r ->
-		mkt_app lcons [mkt_app tpexpr [Lazy.force tz];t;r])
-	     lt
-	     (mkt_app lnil [mkt_app tpexpr [Lazy.force tz]]) in
-	 mkt_app lcons [tlp ();ltterm;r])
+         let ltterm =
+           List.fold_right
+             (fun t r ->
+                mkt_app lcons [mkt_app tpexpr [Lazy.force tz];t;r])
+             lt
+             (mkt_app lnil [mkt_app tpexpr [Lazy.force tz]]) in
+         mkt_app lcons [tlp ();ltterm;r])
       res
       (mkt_app lnil [tlp ()]) in
   sinfo "term computed";
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 071c74ab9b..9a22f39f84 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -181,7 +181,7 @@ let norm p = match p with
      let d = (Array.length a -1) in
      let n = ref d in
        while !n>0 && (equal a.(!n) (Pint coef0)) do
-	 n:=!n-1;
+         n:=!n-1;
        done;
        if !n<0 then Pint coef0
        else if Int.equal !n 0 then a.(0)
@@ -222,7 +222,7 @@ let coef v i p =
 let rec plusP p q =
   let res =
     (match (p,q) with
-	 (Pint a,Pint b) -> Pint (C.plus a b)
+         (Pint a,Pint b) -> Pint (C.plus a b)
        |(Pint a, Prec (y,q1)) -> let q2=Array.map copyP q1 in
            q2.(0)<- plusP p q1.(0);
            Prec (y,q2)
@@ -317,7 +317,7 @@ let deriv v p =
          else
            (let p2 = Array.make d (Pint coef0) in
               for i=0 to d-1 do
-		p2.(i)<- multP (Pint (coef_of_int (i+1))) p1.(i+1);
+                p2.(i)<- multP (Pint (coef_of_int (i+1))) p1.(i+1);
               done;
               Prec (x,p2))
     | Prec(x,p1)-> Pint coef0
@@ -416,37 +416,37 @@ let rec string_of_Pcut p =
     for i=(Array.length t)-1 downto 1 do
       if (!nsP)<0
       then (sp:="...";
-	    if not (!fin) then s:=(!s)^"+"^(!sp);
-	    fin:=true)
+            if not (!fin) then s:=(!s)^"+"^(!sp);
+            fin:=true)
       else (
-	let si=string_of_Pcut  t.(i) in
-	sp:="";
-	if Int.equal i 1
-	then (
-	  if not (String.equal si "0")
-	  then (nsP:=(!nsP)-1;
-		if String.equal si "1"
-		then sp:=v
-		else
-		  (if (String.contains si '+')
-		  then sp:="("^si^")*"^v
-		  else sp:=si^"*"^v)))
-	else (
-	  if not (String.equal si "0")
-	  then (nsP:=(!nsP)-1;
-		if String.equal si "1"
-		then sp:=v^"^"^(string_of_int i)
-		else (if (String.contains si '+')
-		then sp:="("^si^")*"^v^"^"^(string_of_int i)
-		else  sp:=si^"*"^v^"^"^(string_of_int i))));
-	if not (String.is_empty !sp) && not (!fin)
-	then (nsP:=(!nsP)-1;
-	      if String.is_empty !s
-	      then s:=!sp
-	      else s:=(!s)^"+"^(!sp)));
+        let si=string_of_Pcut  t.(i) in
+        sp:="";
+        if Int.equal i 1
+        then (
+          if not (String.equal si "0")
+          then (nsP:=(!nsP)-1;
+                if String.equal si "1"
+                then sp:=v
+                else
+                  (if (String.contains si '+')
+                  then sp:="("^si^")*"^v
+                  else sp:=si^"*"^v)))
+        else (
+          if not (String.equal si "0")
+          then (nsP:=(!nsP)-1;
+                if String.equal si "1"
+                then sp:=v^"^"^(string_of_int i)
+                else (if (String.contains si '+')
+                then sp:="("^si^")*"^v^"^"^(string_of_int i)
+                else  sp:=si^"*"^v^"^"^(string_of_int i))));
+        if not (String.is_empty !sp) && not (!fin)
+        then (nsP:=(!nsP)-1;
+              if String.is_empty !s
+              then s:=!sp
+              else s:=(!s)^"+"^(!sp)));
     done;
     if String.is_empty !s then (nsP:=(!nsP)-1;
-		   (s:="0"));
+                   (s:="0"));
     !s
 
 let to_string p =
@@ -471,10 +471,10 @@ let rec quo_rem_pol p q x =
   if Int.equal x 0
   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)
+          |_ -> assert false)
   else
     let m = deg x q in
     let b = coefDom x q in
@@ -483,14 +483,14 @@ let rec quo_rem_pol p q x =
     let s = ref cf0 in
     let continue =ref true in
       while (!continue) && (not (equal !r cf0)) do
-	let n = deg x !r in
-	  if n<m
-	  then continue:=false
-	  else (
+        let n = deg x !r in
+          if n<m
+          then continue:=false
+          else (
             let a = coefDom x !r in
             let p1 = remP x !r in  (* r = a*x^n+p1 *)
             let c = div_pol a b (x-1) in  (* a = c*b *)
-	    let s1 = c @@ ((monome x (n-m))) in
+            let s1 = c @@ ((monome x (n-m))) in
               s:= plusP (!s) s1;
               r:= p1 -- (s1 @@ q1);
           )
@@ -503,11 +503,11 @@ and div_pol p q x =
     if equal r cf0
     then s
     else  failwith ("div_pol:\n"
-		   ^"p:"^(to_string p)^"\n"
-		   ^"q:"^(to_string q)^"\n"
-		   ^"r:"^(to_string r)^"\n"
-		   ^"x:"^(string_of_int x)^"\n"
-		   )
+                   ^"p:"^(to_string p)^"\n"
+                   ^"q:"^(to_string q)^"\n"
+                   ^"r:"^(to_string r)^"\n"
+                   ^"x:"^(string_of_int x)^"\n"
+                   )
 let divP p q=
   let x = max (max_var_pol p) (max_var_pol q) in
   div_pol p q x
@@ -534,29 +534,29 @@ let pseudo_div p q x =
       Pint _ -> (cf0, q,1, p)
     | Prec (v,q1) when not (Int.equal x v) -> (cf0, q,1, p)
     | Prec (v,q1) ->
-	(
-	  (*  pr "pseudo_division: c^d*p = s*q + r";*)
-	  let delta = ref 0 in
-	  let r = ref p in
-	  let c = coefDom x q in
-	  let q1 = remP x q in
-	  let d' = deg x q in
-	  let s = ref cf0 in
-	    while (deg x !r)>=(deg x q) do
-	      let d = deg x !r in
-	      let a = coefDom x !r in
-	      let r1=remP x !r in
-	      let u = a @@ ((monome x (d-d'))) in
-		r:=(c @@ r1) -- (u @@ q1);
-		s:=plusP (c @@ (!s)) u;
-		delta := (!delta) + 1;
-	    done;
-	    (*
-	      pr ("deg d: "^(string_of_int (!delta))^", deg c: "^(string_of_int (deg_total c)));
-	      pr ("deg r:"^(string_of_int (deg_total !r)));
-	    *)
-	    (!r,c,!delta, !s)
-	)
+        (
+          (*  pr "pseudo_division: c^d*p = s*q + r";*)
+          let delta = ref 0 in
+          let r = ref p in
+          let c = coefDom x q in
+          let q1 = remP x q in
+          let d' = deg x q in
+          let s = ref cf0 in
+            while (deg x !r)>=(deg x q) do
+              let d = deg x !r in
+              let a = coefDom x !r in
+              let r1=remP x !r in
+              let u = a @@ ((monome x (d-d'))) in
+                r:=(c @@ r1) -- (u @@ q1);
+                s:=plusP (c @@ (!s)) u;
+                delta := (!delta) + 1;
+            done;
+            (*
+              pr ("deg d: "^(string_of_int (!delta))^", deg c: "^(string_of_int (deg_total c)));
+              pr ("deg r:"^(string_of_int (deg_total !r)));
+            *)
+            (!r,c,!delta, !s)
+        )
 
 (* gcd with subresultants *)
 
@@ -581,28 +581,28 @@ and pgcd_coef_pol c p x =
 
 and pgcd_pol_rec p q x =
  match (p,q) with
-	(Pint a,Pint b) -> Pint (C.pgcd (C.abs a) (C.abs b))
+        (Pint a,Pint b) -> Pint (C.pgcd (C.abs a) (C.abs b))
       |_ ->
-	  if equal p cf0
-	  then q
-	  else if equal q cf0
-	  then p
-	  else if Int.equal (deg x q) 0
-	  then pgcd_coef_pol q p x
-	  else if Int.equal (deg x p) 0
-	  then pgcd_coef_pol p q x
-	  else (
-	    let a = content_pol p x in
-	    let b = content_pol q x in
-	    let c = pgcd_pol_rec a b (x-1) in
-	    pr (string_of_int x);
-	    let p1 = div_pol p c x in
-	    let q1 = div_pol q c x in
-	    let r = gcd_sub_res p1 q1 x in
-	    let cr = content_pol r x in
-	    let res = c @@ (div_pol r cr x) in
-	    res
-	   )
+          if equal p cf0
+          then q
+          else if equal q cf0
+          then p
+          else if Int.equal (deg x q) 0
+          then pgcd_coef_pol q p x
+          else if Int.equal (deg x p) 0
+          then pgcd_coef_pol p q x
+          else (
+            let a = content_pol p x in
+            let b = content_pol q x in
+            let c = pgcd_pol_rec a b (x-1) in
+            pr (string_of_int x);
+            let p1 = div_pol p c x in
+            let q1 = div_pol q c x in
+            let r = gcd_sub_res p1 q1 x in
+            let cr = content_pol r x in
+            let res = c @@ (div_pol r cr x) in
+            res
+           )
 
 (* Sub-résultants:
 
@@ -630,10 +630,10 @@ and gcd_sub_res p q x =
       if d<d'
       then gcd_sub_res q p x
       else
-	let delta = d-d' in
-	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
+        let delta = d-d' in
+        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