new exception captured

[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 7ea11f3120035edaf8d4c63e43f7be8830c270fd..d812279b8c68eed15d00c337da7f0dd821dccd0b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -99,7 +99,6 @@ let rec typeof
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion metasenv subst context term expty 
 =
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
   let force_ty metasenv subst context orig t infty expty =
     (*D*)inside 'F'; try let rc = 
     match expty with