From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 22 Apr 2008 12:48:10 +0000 (+0000)
Subject: added a call to ppcontext in the case of appl, to ease the localization of the error
X-Git-Tag: make_still_working~5300
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28a4c3ee256336c0f482235f81b8bd5ad622945a;p=helm.git

added a call to ppcontext in the case of appl, to ease the localization of the error
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f6d8d8902..e96169e3e 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -350,11 +350,12 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
                   ("Appl: wrong application of %s: the parameter %s has type"^^
-                   "\n%s\nbut it should have type \n%s\n")
+                   "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
                   (NCicPp.ppterm ~subst ~metasenv ~context he)
                   (NCicPp.ppterm ~subst ~metasenv ~context arg)
                   (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
-                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
+                  (NCicPp.ppterm ~subst ~metasenv ~context s)
+                  (NCicPp.ppcontext ~subst ~metasenv context))))
        | _ ->
           raise 
             (TypeCheckerFailure