From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Jul 2009 19:43:54 +0000 (+0000)
Subject: Debugging printf removed
X-Git-Tag: make_still_working~3645
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0e7d31c2ea6beafc094abed7ef9f34602195f85;p=helm.git

Debugging printf removed
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 71203b3a5..be7a2fe4c 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -159,16 +159,11 @@ let rec lambda_intros rdb metasenv subst context t args =
 let metasenv,subst,_,_ =
  !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None
 in
-prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty);
-prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args);
-prerr_endline (NCicPp.ppmetasenv metasenv ~subst);
        let metasenv,subst =
         unify rdb true metasenv subst context_of_args meta_applied ty in
-prerr_endline "UNIFY FINITA";
        let telescopic_ty = NCicSubstitution.lift n instance in
        let telescopic_ty =
         mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in
-prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty);
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
          (arg::processed_args) tail
@@ -354,7 +349,6 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                  let metasenv, subst, lambda_Mj =
                    lambda_intros rdb metasenv subst context t1 args
                  in
-prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj);
                    unify rdb test_eq_only metasenv subst context 
                     (C.Meta (i,l)) lambda_Mj,
                    i