From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 21:13:18 +0000 (+0000)
Subject: Error message improved.
X-Git-Tag: make_still_working~5392
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97b4064d9c578ba0e944282d5b465419488dbd33;p=helm.git

Error message improved.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 2f43659e8..3d0f13e2b 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -557,7 +557,10 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected\n%s\nfound\n%s")
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut is should have type \n%s\n")
+                  (NCicPp.ppterm ~subst ~metasenv ~context he)
+                  (NCicPp.ppterm ~subst ~metasenv ~context arg)
                   (NCicPp.ppterm ~subst ~metasenv ~context s)
                   (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
        | _ ->