X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=1de72fb5d2d7368da9eba47a0301017e7fe7a742;hb=c137ba88f68a47e567077909a23993c3c8c9854d;hp=326d9e2c28a882c6eb4f5dcb1a398318d9b2636e;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

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