From 8465f33f9ad62040f41a2a2604745cda11725d98 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Feb 2007 14:53:30 +0000
Subject: [PATCH] Debugging code removed.

---
 components/tactics/primitiveTactics.ml | 1 -
 1 file changed, 1 deletion(-)

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
-- 
2.39.2