X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=fdb9c2137332b3c5196b3b10349f1a046b983723;hb=0bcc03be833e8f177850e6b9785713d7975ee8bd;hp=8c92d3328b8556e9ecb91912e140a6f09dee3736;hpb=0db291bf647ae5d8aa54c58691ab170b46e7666a;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8c92d3328..fdb9c2137 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -74,7 +74,7 @@ let exp_implicit rdb ~localise metasenv subst context with_type t =
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->
-               raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type")))
+               raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type: " ^ NCicPp.ppterm ~metasenv ~subst ~context typ)))
 
            in
             metasenv,subst,Some typ