Error message improved.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 2f43659e823d5a547d6603bcc56150b619227b8d..3d0f13e2b582440fcc99af9ef83b78411d06acb0 100644 (file)
--- 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))))
        | _ ->