Improved 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 d279b840b18d0fcc8602bff628677e7d32967dc3..8872cbc9b576f855a8f65334addc871864e3bc6c 100644 (file)
--- 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 =