removed debug prerr_endline

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c1823d1c9d3af3a12cc4a4d701ea9590cea56b4a..e2fac6167bae90cd10c8e8c5df2b3a2eadaab434 100644 (file)
--- 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