From 0e135d52a8c1b825a7844b897546bb7ae4af44d2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:13:10 +0000 Subject: [PATCH] Improved error message. --- helm/software/components/ng_refiner/nCicRefiner.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index d279b840b..8872cbc9b 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -714,7 +714,8 @@ let typeof_obj raise (RefineFailure (lazy (localise te, - "Non positive occurence in " ^ NUri.string_of_uri uri))) + "Non positive occurence in " ^ + NCicPp.ppterm ~metasenv ~subst ~context te))) else let relsno = List.length itl + leftno in let te = -- 2.39.2