]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 14:53:30 +0000 (14:53 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 14:53:30 +0000 (14:53 +0000)
helm/software/components/tactics/primitiveTactics.ml

index d716ed2d480cc77e7c40c7515a1b03d049322705..3ef39d0c512dbb52c6b35398b78d1199ca02dc83 100644 (file)
@@ -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