* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
* ...") *)
raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) "")))
;;
-let debug_print = fun _ -> () ;;
+let debug_print = fun _ -> ();;
let rec split l n =
match (l,n) with
let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
if not b then
raise (TypeCheckerFailure
- (lazy "the type of the body is not the one expected"))
+ (lazy
+ ("the type of the body is not the one expected:\n" ^
+ CicPp.ppterm ty_te ^ "\nvs\n" ^
+ CicPp.ppterm ty)))
else
ugraph
| C.Constant (_,None,ty,_,_) ->