bug in hypotesis parsing solved

[helm.git] / helm / gTopLevel / fourier.ml

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index 3704bf67bb388e3e23973d3b50db35144e9d25fd..d7728c0b338e7b4fa12066c60007463dcef530e4 100644 (file)
--- 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
 ;;