From d3578004b25e8883581d78b3173c55ab60987299 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 12 Feb 2004 12:57:39 +0000 Subject: [PATCH] removed some anciente debugging messages --- helm/ocaml/tactics/primitiveTactics.ml | 2 -- 1 file changed, 2 deletions(-) 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 -- 2.39.2