Debugging code removed.

[helm.git] / helm / software / components / tactics / primitiveTactics.ml

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index d716ed2d480cc77e7c40c7515a1b03d049322705..3ef39d0c512dbb52c6b35398b78d1199ca02dc83 100644 (file)
--- 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