debug pps removed

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8edf316f695222e86dab1343fb360af59e46029d..4abfc933eb7b59b83b413d07c1128e4e92d3ea37 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -975,7 +975,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               subst_metasenv_and_fix_names nstatus)
             nstatus tacl
          in
-         NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
          `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->