From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Feb 2007 14:53:30 +0000 (+0000)
Subject: Debugging code removed.
X-Git-Tag: make_still_working~6466
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=275bf791887670020301eb6160d540d00d368e76;p=helm.git

Debugging code removed.
---

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index d716ed2d4..3ef39d0c5 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -628,7 +628,6 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
        let term_to_refine =
         C.MutCase (uri,typeno,outtype,term,patterns)
        in
-prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
         let refined_term,_,metasenv'',_ = 
          CicRefine.type_of_aux' metasenv' context term_to_refine
            CicUniv.empty_ugraph