From f541206af7fccf9de78b31d8f2aaf5f786f63d1f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 11:06:26 +0000 Subject: [PATCH] removed debug prerr_endline --- helm/ocaml/tactics/primitiveTactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c1823d1c9..e2fac6167 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -333,8 +333,8 @@ let apply_tac_verbose ~term (proof, goal) = let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in - prerr_endline ("term:" ^ CicPp.ppterm term); - prerr_endline ("termty:" ^ CicPp.ppterm termty); +(* prerr_endline ("term:" ^ CicPp.ppterm term);*) +(* prerr_endline ("termty:" ^ CicPp.ppterm termty);*) let subst,newmetasenv',t = try new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty -- 2.39.2