]> matita.cs.unibo.it Git - helm.git/blobdiff - components/cic_unification/cicRefine.ml
removed ugly printings
[helm.git] / components / cic_unification / cicRefine.ml
index d6504eb1584c28c5ec7abd5ff4d190e1daa7135b..840a955cb8a7218749b74aeed1203ab52485004f 100644 (file)
@@ -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