From 1b1a51a03ebfc8b16df3731729f857377183425f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Oct 2009 08:16:10 +0000 Subject: [PATCH] Improved 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 e2aabb31c..b84c23aae 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -377,7 +377,7 @@ and try_coercions rdb let rec first exc = function | [] -> raise (wrap_exc (lazy (localise orig_t, Printf.sprintf - "The term %s has type %s but is here used with type %s" + "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (NCicPp.ppterm ~metasenv ~subst ~context t) (NCicPp.ppterm ~metasenv ~subst ~context infty) (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) -- 2.39.2