- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[helm.git] / helm / software / helena / src / common / output.ml

diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml
index 94bf217daec407fd56619e2b11d0dc834fde7626..3c813b275c76fe3d5105f4442684157955fca6ce 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -43,6 +43,7 @@ let add
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
 =
+(*
    if !G.ct >= level then begin
       if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
       if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
@@ -50,6 +51,7 @@ let add
       if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
       if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
    end;
+*)
 reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;