X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=840a955cb8a7218749b74aeed1203ab52485004f;hb=241dd3fc882e24a1d3a386a9c612aa8fc720abdb;hp=d6504eb1584c28c5ec7abd5ff4d190e1daa7135b;hpb=e70d9b498615e473258fb1010cc65d39e27a5830;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index d6504eb15..840a955cb 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -677,8 +677,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              type_of_aux subst metasenv context expected_type ugraph1
            in
            let actual_type = CicReduction.whd ~subst context actual_type in
-           prerr_endline (CicPp.ppterm expected_type');
-           prerr_endline (CicPp.ppterm actual_type);
            let subst,metasenv,ugraph3 =
             try
              fo_unif_subst subst context metasenv