X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=8872cbc9b576f855a8f65334addc871864e3bc6c;hb=0e135d52a8c1b825a7844b897546bb7ae4af44d2;hp=d279b840b18d0fcc8602bff628677e7d32967dc3;hpb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;p=helm.git 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 =