Debugging printf removed

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 71203b3a5dccdf2b3c5207677f2df501c6eb4084..be7a2fe4cab899551151f4745d5fed2851d57cd1 100644 (file)
--- 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