From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 18 Jan 2005 18:15:57 +0000 (+0000)
Subject: removed spurious debugging prints
X-Git-Tag: V_0_1_0~131
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea71e96f90757766465abbdd22aec34d095dbf1d;p=helm.git

removed spurious debugging prints
---

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 1864e89b0..d87d7eb4f 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -346,8 +346,6 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 prerr_endline (CicPp.ppterm eliminator_type);
 prerr_endline (CicPp.ppterm eliminator_body);
 *)
-prerr_endline "generato l'eliminatore";
-prerr_endline "inizio type checking";
       let (computed_type, ugraph) =
         try
           CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
@@ -356,8 +354,6 @@ prerr_endline "inizio type checking";
             "type checker failure while type checking:\n%s\nerror:\n%s"
             (CicPp.ppterm eliminator_body) msg))
       in
-prerr_endline "fine type checking";
-prerr_endline "inizio are convertible";
       if not (fst (CicReduction.are_convertible []
         eliminator_type computed_type ugraph))
       then