X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ffourier.ml;h=d7728c0b338e7b4fa12066c60007463dcef530e4;hb=81cc12ae4ebd9741585b38f41c7fb5eb6c5ae916;hp=3704bf67bb388e3e23973d3b50db35144e9d25fd;hpb=c6b222d016300d3b123a4d1863c048b950292844;p=helm.git

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index 3704bf67b..d7728c0b3 100644
--- a/helm/gTopLevel/fourier.ml
+++ b/helm/gTopLevel/fourier.ml
@@ -171,12 +171,14 @@ let deduce_add lneg lpos =
 (* élimination de la première variable à partir d'une liste d'inéquations:
 opération qu'on itère dans l'algorithme de Fourier.
 *)
-let deduce1 s =
+let deduce1 s i=
     match (partitionne s) with 
       [lneg;lnul;lpos] ->
-    let lnew = deduce_add lneg lpos in
-    (List.map ie_tl lnul)@lnew
-     |_->assert false
+         let lnew = deduce_add lneg lpos in
+	 (match lneg with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->();
+	  match lpos with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->());
+         (List.map ie_tl lnul)@lnew
+   |_->assert false
 ;;
 (* algorithme de Fourier: on élimine successivement toutes les variables.
 *)
@@ -184,7 +186,7 @@ let deduce lie =
    let n = List.length (fst (List.hd lie)) in
    let lie=ref (add_hist lie) in
    for i=1 to n-1 do
-      lie:= deduce1 !lie;
+      lie:= deduce1 !lie i;
    done;
    !lie
 ;;