Better error message.

[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 8c92d3328b8556e9ecb91912e140a6f09dee3736..fdb9c2137332b3c5196b3b10349f1a046b983723 100644 (file)
--- 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