debug pps removed

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ffa2422e4afc21151992e7a5f3e8510ad20e19ad..6bcda0df86781d8abe3f61bc5334bed860a2b6e3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -558,7 +558,6 @@ let undebruijnate inductive ref t rev_fl =
 let typeof_obj 
   rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
 = 
-prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
   let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
     let metasenv, subst, ty, sort = 
       typeof rdb ~localise metasenv subst context ty None