From ee641910c2496cd531c90cad25ffbe08591ca5df Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Dec 2008 23:02:10 +0000 Subject: [PATCH] Debugging instructions removed. --- helm/software/components/ng_refiner/nCicCoercion.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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) ;; -- 2.39.2