exportation to \lambda\delta representation in elpi

[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 23829c095ff543aedfe7afe9db4eaf6e88a79776..a72f94318d785686562302c3ddb80d04c4b0157a 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -41,7 +41,15 @@ let clear_reductions () = reductions := initial_reductions
 let add 
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
-= reductions := {
+=
+(*
+ if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
+ if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
+ if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
+ if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
+ if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
+*) 
+reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
    theta = !reductions.theta + theta;