removed spurious debugging prints

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 1864e89b0c202d39217466fe459988270d608ce9..d87d7eb4fdd991654f79fc035596b52a2c843c6e 100644 (file)
--- 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