debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
fast_eq_check unit_eq status j
with
+ | NCicEnvironment.ObjectNotFound s as e ->
+ raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
let smart_apply_tac t s =
oldstatus#set_status s
in
let s = up_to depth depth in
- print (print_stat statistics);
+ debug_print (print_stat statistics);
debug_print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
debug_print(lazy