| `Reduce -> "reduce"
| `Simpl -> "simplify"
| `Whd -> "whd"
+ | `Normalize -> "normalize"
let rec pp_tactic = function
| Absurd (_, term) -> "absurd" ^ pp_term_ast term
| Reduce (_, kind, Some (terms, `Everywhere)) ->
sprintf "%s in hyp %s" (pp_reduction_kind kind)
(String.concat ", " (List.map pp_term_ast terms))
+ | ReduceAt (_, kind, id, term) ->
+ sprintf "%s %s at %s" (pp_reduction_kind kind) id
+ (pp_term_ast term)
| Reflexivity _ -> "reflexivity"
| Replace (_, t1, t2) ->
sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
| WElim (_, t) -> "whelp elim " ^ pp_term t
| WMatch (_, term) -> "whelp match " ^ pp_term term
(* real macros *)
- | Abort _ -> "Abort"
+(* | Abort _ -> "Abort" *)
| Check (_, term) -> sprintf "Check %s" (pp_term term)
| Hint _ -> "hint"
- | Redo (_, None) -> "Redo"
- | Redo (_, Some n) -> sprintf "Redo %d" n
+(* | Redo (_, None) -> "Redo"
+ | Redo (_, Some n) -> sprintf "Redo %d" n *)
| Search_pat (_, kind, pat) ->
sprintf "search %s \"%s\"" (pp_search_kind kind) pat
| Search_term (_, kind, term) ->
sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
- | Undo (_, None) -> "Undo"
- | Undo (_, Some n) -> sprintf "Undo %d" n
+(* | Undo (_, None) -> "Undo"
+ | Undo (_, Some n) -> sprintf "Undo %d" n *)
| Print (_, name) -> sprintf "Print \"%s\"" name
| Quit _ -> "Quit"