let rec pp_tactic = function
| LocatedTactic (loc, tac) -> pp_tactic tac
- | Absurd -> "absurd"
+ | Absurd term -> "absurd" ^ pp_term term
| Apply term -> "apply " ^ pp_term term
| Assumption -> "assumption"
| Change (t1, t2, where) ->
| Fold (kind, term) ->
sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
| Fourier -> "fourier"
+ | Hint -> "hint"
| Injection ident -> "injection " ^ ident
| Intros (num, idents) ->
sprintf "intros%s%s"
| Symmetry -> "symmetry"
| Transitivity term -> "transitivity " ^ pp_term term
+let pp_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Goal -> "Goal"
+ | `Lemma -> "Lemma"
+ | `Remark -> "Remark"
+ | `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"
+ | Redo None -> "Redo"
+ | Redo (Some n) -> sprintf "Redo %d" n
+ | Theorem (flavour, name, typ, body) ->
+ sprintf "%s %s: %s %s"
+ (pp_flavour flavour)
+ (match name with None -> "" | Some name -> name)
+ (CicAstPp.pp_term typ)
+ (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
+
+ | Tactic tac -> pp_tactic tac
+ | Command cmd -> pp_command cmd
+
| 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
- | Tactic tac -> pp_tactic tac
| Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
| Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs)
| Try tac -> "try " ^ pp_tactical tac