| `Normalize -> "normalize"
-let pp_pattern (hyp, goal) =
+let pp_pattern (t, hyp, goal) =
let pp_hyp_pattern l =
String.concat "; "
- (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l)
+ (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in
+ let pp_t t =
+ match t with
+ None -> ""
+ | Some t -> pp_term_ast t
in
- let pp_goal_pattern p =
- match p with
- | None -> ""
- | Some p -> pp_term_ast p
- in
- let separator =
- if hyp <> [] then " \\vdash " else " "
- in
- "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal
+ pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
let rec pp_tactic = function
| Absurd (_, term) -> "absurd" ^ pp_term_ast term
| Apply (_, term) -> "apply " ^ pp_term_ast term
| Auto _ -> "auto"
| Assumption _ -> "assumption"
- | Change (_, t1, t2, where) ->
- sprintf "change %s with %s %s" (pp_term_ast t1) (pp_term_ast t2)
- (pp_pattern where)
+ | Change (_, where, with_what) ->
+ sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what)
| Clear (_,id) -> sprintf "clear %s" id
| ClearBody (_,id) -> sprintf "clearbody %s" id
| Compare (_,term) -> "compare " ^ pp_term_ast term
| ElimType (_, term) -> "elim type " ^ pp_term_ast term
| Exact (_, term) -> "exact " ^ pp_term_ast term
| Exists _ -> "exists"
- | 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)
+ | Fold (_, kind, pattern) ->
+ sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+ | Generalize (_, pattern, ident) ->
+ sprintf "generalize %s%s" (pp_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
- (pp_pattern pattern)
| Goal (_, n) -> "goal " ^ string_of_int n
| Fail _ -> "fail"
| Fourier _ -> "fourier"