From 97b4064d9c578ba0e944282d5b465419488dbd33 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 21:13:18 +0000 Subject: [PATCH] Error message improved. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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)))) | _ -> -- 2.39.2