| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"
- | Rename (_, froms, tos) ->
- sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos)
| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
| Rewrite (_, pos, t, pattern, names) ->
let pp_macro ~term_pp =
let term_pp = pp_arg ~term_pp in
let style_pp = function
- | Declarative -> ""
- | Procedural -> "procedural "
+ | Declarative -> ""
+ | Procedural None -> "procedural "
+ | Procedural (Some i) -> sprintf "procedural %u " i
in
let prefix_pp prefix =
if prefix = "" then "" else sprintf " \"%s\"" prefix