From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Jun 2005 11:06:26 +0000 (+0000)
Subject: removed debug prerr_endline
X-Git-Tag: PRE_INDEX_1~80
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f541206af7fccf9de78b31d8f2aaf5f786f63d1f;p=helm.git

removed debug prerr_endline
---

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