]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/output.ml
new syntax of abstractions propagated to complete_rg
[helm.git] / helm / software / helena / src / common / output.ml
index 013287243d5e1e0aaebe03b5b0390492a49909c8..d84012c2f1d706876fbcf8c8e1a6e63be3f0eb6d 100644 (file)
@@ -43,13 +43,11 @@ 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 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);
-*) 
+ if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
 reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;