From: Claudio Sacerdoti Coen Date: Fri, 5 Dec 2008 23:02:44 +0000 (+0000) Subject: Debugging code removed X-Git-Tag: make_still_working~4446 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e81a9ef7aca4ef1715a39524d0df2d2c18c124df;p=helm.git Debugging code removed --- diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7ea11f312..d812279b8 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -99,7 +99,6 @@ let rec typeof ?(localise=fun _ -> Stdpp.dummy_loc) ~look_for_coercion metasenv subst context term expty = - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term); let force_ty metasenv subst context orig t infty expty = (*D*)inside 'F'; try let rc = match expty with