| Qed name ->
(match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
| Quit -> "Quit"
+ | Redo None -> "Redo"
+ | Redo (Some n) -> sprintf "Redo %d" n
| Theorem (flavour, name, typ, body) ->
sprintf "%s %s: %s %s"
(pp_flavour flavour)
(match body with
| None -> ""
| Some body -> "\\def " ^ CicAstPp.pp_term body)
+ | Undo None -> "Undo"
+ | Undo (Some n) -> sprintf "Undo %d" n
let rec pp_tactical = function
| LocatedTactical (loc, tac) -> pp_tactical tac