| Discriminate ident -> "discriminate " ^ ident
| Elim (term, using) ->
sprintf "elim " ^ pp_term term ^
- (match using with None -> "" | Some term -> "using " ^ pp_term term)
+ (match using with None -> "" | Some term -> " using " ^ pp_term term)
| ElimType term -> "elim type " ^ pp_term term
| Exact term -> "exact " ^ pp_term term
| Exists -> "exists"
| Intros (num, idents) ->
sprintf "intros%s%s"
(match num with None -> "" | Some num -> " " ^ string_of_int num)
- (match idents with [] -> "" | idents -> pp_idents idents)
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
| Left -> "left"
| LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
| Reduce (_, _, _) -> assert false (* TODO *)
| 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
+ | Proof -> "Proof."
+ | 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)
+ | 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
+
+ | 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)
+ | 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
and pp_tacticals tacs = String.concat "; " (List.map pp_tactical tacs)
+let pp_tactical tac = pp_tactical tac ^ "."
+