summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
9af2c02)
* better pretty-printing of type-checking exceptions
* http://helm.cs.unibo.it/
*)
* http://helm.cs.unibo.it/
*)
let conffile = "../../../matita/matita.conf.xml"
let _ = CicEnvironment.set_trust (fun _ -> trust);;
let conffile = "../../../matita/matita.conf.xml"
let _ = CicEnvironment.set_trust (fun _ -> trust);;
| exn ->
Printf.printf "\e[0;31mFAIL\e[0m\n";
flush stdout;
| exn ->
Printf.printf "\e[0;31mFAIL\e[0m\n";
flush stdout;
- prerr_endline (Printexc.to_string exn)
+ prerr_endline
+ (match exn with
+ CicTypeChecker.TypeCheckerFailure msg ->
+ "TypeCheckerFailure: " ^ Lazy.force msg
+ | CicTypeChecker.AssertFailure msg ->
+ "TypeCheckerAssertion: " ^ Lazy.force msg
+ | _ -> Printexc.to_string exn)