Names of some constructors changed.

[helm.git] / helm / gTopLevel / doubleTypeInference.ml

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index b9a79b64ff74b0ec71eb80e54e8024a224a6984c..024f49ebf6732ca6bf4ad6e82d5011007c1012b7 100644 (file)
--- 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