X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=3ef39d0c512dbb52c6b35398b78d1199ca02dc83;hb=8465f33f9ad62040f41a2a2604745cda11725d98;hp=d716ed2d480cc77e7c40c7515a1b03d049322705;hpb=e00d05ab58597620345c2fd49b84a23efa8db34c;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index d716ed2d4..3ef39d0c5 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/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