let tactical_terminator = "."
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
-let tactical_separator = ";"
let pp_term_ast term = CicAstPp.pp_term term
let pp_term_cic term = CicPp.ppterm term
| `Lemma -> "Lemma"
| `Remark -> "Remark"
| `Theorem -> "Theorem"
+ | `Variant -> "Variant"
let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| `Match -> "match"
| `Elim -> "elim"
+ | `Instance -> "instance"
let pp_macro pp_term = function
(* Whelp *)
"record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
pp_fields fields ^ "}"
-
let pp_command = function
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
| Tactic (_, tac) -> pp_tactic tac
| Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
| Repeat (_, tac) -> "repeat " ^ pp_tactical tac
- | Seq (_, tacs) -> pp_tacticals tacs
+ | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
| Then (_, tac, tacs) ->
- sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
- | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+ sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+ | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical tac
+ | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
-and pp_tacticals tacs =
- String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs)
+and pp_tacticals ~sep tacs =
+ String.concat sep (List.map pp_tactical tacs)
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
let pp_tactic tac = pp_tactic tac ^ tactic_terminator