| Some p -> pp_term_ast p
in
let separator =
- if hyp <> [] then " \vdash " else " "
+ if hyp <> [] then " \\vdash " else " "
in
"in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal
| Auto _ -> "auto"
| Assumption _ -> "assumption"
| Change (_, t1, t2, where) ->
- sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2)
+ sprintf "change %s with %s %s" (pp_term_ast t1) (pp_term_ast t2)
(pp_pattern where)
+ | Clear (_,id) -> sprintf "clear %s" id
+ | ClearBody (_,id) -> sprintf "clearbody %s" id
| Compare (_,term) -> "compare " ^ pp_term_ast term
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| ElimType (_, term) -> "elim type " ^ pp_term_ast term
| Exact (_, term) -> "exact " ^ pp_term_ast term
| Exists _ -> "exists"
- | Fold (_, kind, term) ->
- sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
+ | Fold (_, kind, term, pattern) ->
+ sprintf "fold %s %s %s" (pp_reduction_kind kind) (pp_term_ast term)
+ (pp_pattern pattern)
| Generalize (_, term, ident, pattern) ->
sprintf "generalize %s%s %s" (pp_term_ast term)
(match ident with None -> "" | Some id -> " as " ^ id)
(pp_pattern pattern)
| Goal (_, n) -> "goal " ^ string_of_int n
+ | Fail _ -> "fail"
| Fourier _ -> "fourier"
+ | IdTac _ -> "id"
| Injection (_, term) -> "injection " ^ pp_term_ast term
| Intros (_, None, []) -> "intro"
| Intros (_, num, idents) ->
| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat)
| Reflexivity _ -> "reflexivity"
- | Replace (_, t1, t2) ->
- sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
+ | Replace (_, pattern, t) ->
+ sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t)
| Rewrite (_, pos, t, pattern) ->
sprintf "rewrite %s %s %s"
(if pos = `Left then "left" else "right") (pp_term_ast t)
let rec pp_tactical = function
| Tactic (_, tac) -> pp_tactic tac
-
- | Fail _ -> "fail"
| Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
- | IdTac _ -> "id"
| Repeat (_, tac) -> "repeat " ^ pp_tactical tac
| Seq (_, tacs) -> pp_tacticals tacs
| Then (_, tac, tacs) ->