X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=e2fac6167bae90cd10c8e8c5df2b3a2eadaab434;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=c1823d1c9d3af3a12cc4a4d701ea9590cea56b4a;hpb=242e171b023f113228c55ad273797c63becf53e6;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c1823d1c9..e2fac6167 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -333,8 +333,8 @@ let apply_tac_verbose ~term (proof, goal) =
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty
    in
-   prerr_endline ("term:" ^ CicPp.ppterm term);
-   prerr_endline ("termty:" ^ CicPp.ppterm termty);
+(*   prerr_endline ("term:" ^ CicPp.ppterm term);*)
+(*   prerr_endline ("termty:" ^ CicPp.ppterm termty);*)
    let subst,newmetasenv',t = 
      try
        new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty