From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Dec 2008 23:02:10 +0000 (+0000)
Subject: Debugging instructions removed.
X-Git-Tag: make_still_working~4447
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee641910c2496cd531c90cad25ffbe08591ca5df;p=helm.git

Debugging instructions removed.
---

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index b8f31c805..5c79aa95c 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -63,18 +63,17 @@ let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
   let set_src = DB.retrieve_unifiables db_src infty in
   let set_tgt = DB.retrieve_unifiables db_tgt expty in
   let candidates = CoercionSet.inter set_src set_tgt in
-  prerr_endline "aaaaaaaaaaaaa";
   List.map
     (fun (t,arity,arg) ->
         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
         let ty, metasenv, args = 
           NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
         in
-        prerr_endline (
+(*       prerr_endline (
           NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
           NCicPp.ppterm ~metasenv ~subst ~context
           (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
-            string_of_int (List.length args) ^ " == " ^ string_of_int arg);
+            string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
         metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
     (CoercionSet.elements candidates)
 ;;