X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=8a6e8a1c818f5f19a99ff816531a19eb9f3561fc;hb=5d492df3e2715395a554f64dc3f040e13f892974;hp=31768a62dd6ac11e474dca0c2ce997c24c422181;hpb=448920d42f3f7886d27477281b22f0c11771d4ed;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 31768a62d..8a6e8a1c8 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -114,7 +114,13 @@ let look_for_coercion status metasenv subst context infty expty =
 
     List.map
       (fun (t,arity,arg) ->
-          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
+          let ty =
+            try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
+            with NCicTypeChecker.TypeCheckerFailure s ->
+             prerr_endline ("illtyped coercion: "^Lazy.force s);
+             prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+             assert false
+          in
           let ty, metasenv, args = 
            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
           in