let id_tac status = status ;;
let print_tac print_status message status =
- if print_status then pp_status status;
+ if print_status then pp_tac_status status;
prerr_endline message;
status
;;
| `RightToLeft -> "eq" ^ suffix
in
block_tac
- [ select_tac ~where ~job:(`Substexpand 1) true;
+ [ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
("",0,
Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@