X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=dfb014c20d8ada6c609823153632d701b299cee2;hb=c25986cdbd05f0c06d93f850453b5f82695b7814;hp=f1a99408ab80764685a0486deb696eb070f98ec9;hpb=90a9ceff7dc614e7be0b600fc6c820abd980595a;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f1a99408a..dfb014c20 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -557,9 +557,12 @@ 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")
-                  (NCicPp.ppterm ~subst ~metasenv ~context s)
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
+                  ("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 ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
@@ -678,11 +681,11 @@ let rec typeof ~subst ~metasenv context term =
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 (*
-       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
@@ -1064,7 +1067,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with