From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Oct 2009 16:53:34 +0000 (+0000)
Subject: Better error message.
X-Git-Tag: make_still_working~3227
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0bcc03be833e8f177850e6b9785713d7975ee8bd;p=helm.git

Better error message.
---

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