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 f6d8d89025a84e9f9182ab7c601ed68ff5156132..e96169e3e905d36d3f08057825b7971e67f2e0dc 100644 (file)
--- 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