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 =
| _ -> false) trace
;;
-let auto_tac ~params:(univ,flags) status =
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let oldstatus = status in
let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
| _ -> assert false
in
let s = s#set_stack stack in
+ trace_ref := trace;
oldstatus#set_status s
in
let s = up_to depth depth in