X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=024f49ebf6732ca6bf4ad6e82d5011007c1012b7;hb=528294d5228f65f4b3fbd3ebe00a5cd9a8f3b929;hp=b9a79b64ff74b0ec71eb80e54e8024a224a6984c;hpb=d7e5adc6adcdcbc98964fa73b3d8e05cad428a6b;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index b9a79b64f..024f49ebf 100644
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -463,8 +463,6 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
        | Some expectedty' ->
-prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
-prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in