Improved eat_prods error message (at the cost of passing the 6th argument!)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 287cf8cd965d1b6ac0f80466a421427f631ad771..125b66ed35cbd73a945a20a99f4d9d90df1dd8ac 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -539,11 +539,11 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (NCicPp.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-let eat_prods ~subst ~metasenv context ty_he args_with_ty = 
+let eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
   let rec aux ty_he = function 
   | [] -> ty_he
   | (arg, ty_arg)::tl ->
-      (match R.whd ~subst context ty_he with 
+      match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
 (*
           prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
@@ -557,13 +557,20 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected %s, found %s")
+                  ("Appl: wrong parameter-type, expected\n%s\nfound\n%s")
                   (NCicPp.ppterm ~subst ~metasenv ~context s)
                   (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
        | _ ->
           raise 
             (TypeCheckerFailure
-              (lazy "Appl: this is not a function, it cannot be applied")))
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (NCicPp.ppterm ~subst ~metasenv ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args_with_ty - res in
+                   (NCic.Appl
+                    (he::List.map fst
+                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
   in
     aux ty_he args_with_ty
 ;;
@@ -677,7 +684,7 @@ let rec typeof ~subst ~metasenv context term =
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
        ~context) (List.map fst args_with_ty)));
 *)
-       eat_prods ~subst ~metasenv context ty_he args_with_ty
+       eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in