let rec pp_tactic = function
| LocatedTactic (loc, tac) -> pp_tactic tac
- | Absurd -> "absurd"
+ | Absurd term -> "absurd" ^ pp_term term
| Apply term -> "apply " ^ pp_term term
| Assumption -> "assumption"
| Change (t1, t2, where) ->
| Fold (kind, term) ->
sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
| Fourier -> "fourier"
+ | Hint -> "hint"
| Injection ident -> "injection " ^ ident
| Intros (num, idents) ->
sprintf "intros%s%s"