From: Stefano Zacchiroli 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