removed some anciente debugging messages

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