From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Oct 2009 08:16:10 +0000 (+0000)
Subject: Improved error message.
X-Git-Tag: make_still_working~3374
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b1a51a03ebfc8b16df3731729f857377183425f;p=helm.git

Improved error message.
---

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)