From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 12 Feb 2004 12:57:39 +0000 (+0000)
Subject: removed some anciente debugging messages
X-Git-Tag: V_0_3_0~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3578004b25e8883581d78b3173c55ab60987299;p=helm.git

removed some anciente debugging messages
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 326d9e2c2..1de72fb5d 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -265,12 +265,10 @@ let apply_tac ~term ~status:(proof, goal) =
      | _ -> [],newmeta,[],term
    in
    let metasenv' = metasenv@newmetasenvfragment in
-prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; 
    let termty =
     CicSubstitution.subst_vars exp_named_subst_diff
      (CicTypeChecker.type_of_aux' metasenv' context term)
    in
-prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; 
     (* newmeta is the lowest index of the new metas introduced *)
     let (consthead,newmetas,arguments,_) =
      new_metasenv_for_apply newmeta' proof context termty