From 0bcc03be833e8f177850e6b9785713d7975ee8bd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Oct 2009 16:53:34 +0000 Subject: [PATCH] Better error message. --- helm/software/components/ng_refiner/nCicRefiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.5