better error message

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 4b00edd05b2878ccea79ea6712540c2cfaf7db2a..f6d8d89025a84e9f9182ab7c601ed68ff5156132 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1096,16 +1096,12 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
  assert (metasenv = [] && subst = []);
  match kind with
    | C.Constant (_,_,Some te,ty,_) ->
-(*
-      prerr_endline ("TY: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] ty);
-      prerr_endline ("BO: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] te);
-*)
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-(*       prerr_endline "XXXX"; *)
       if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
-       raise (TypeCheckerFailure (lazy (Printf.sprintf
-        "the type of the body is not the one expected:\n%s\nvs\n%s"
+       raise (TypeCheckerFailure (lazy (Printf.sprintf (
+        "the type of the body is not convertible with the declared one.\n"^^
+        "inferred type:\n%s\nexpected type:\n%s")
         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) 
         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty))))
    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)