]> matita.cs.unibo.it Git - helm.git/commitdiff
removed ugly printings
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 23 Jun 2007 14:31:12 +0000 (14:31 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 23 Jun 2007 14:31:12 +0000 (14:31 +0000)
helm/software/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