| `Theorem -> "Theorem"
let pp_command = function
+ | Abort -> "Abort."
+ | Check term -> sprintf "Check %s." (CicAstPp.pp_term term)
| Proof -> "Proof."
+ | Qed name ->
+ (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
+ | Quit -> "Quit."
| Theorem (flavour, name, typ, body) ->
sprintf "%s %s: %s %s."
(pp_flavour flavour)
(match body with
| None -> ""
| Some body -> "\\def " ^ CicAstPp.pp_term body)
- | Qed name ->
- (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
- | Quit -> "Quit."
let rec pp_tactical = function
| LocatedTactical (loc, tac) -> pp_tactical tac