* http://cs.unibo.it/helm/.
*)
-exception RefineFailure of string;;
+type failure_msg
+exception RefineFailure of failure_msg;;
exception Uncertain of string;;
exception AssertFailure of string;;
+val explain_error: failure_msg -> string
+
(* type_of_aux' metasenv context term graph *)
(* refines [term] and returns the refined form of [term], *)
(* its type, the new metasenv and universe graph. *)