"cut " ^ pp_term_ast term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| DecideEquality _ -> "decide equality"
- | Decompose (_, term) ->
- sprintf "decompose %s" (pp_term_ast term)
+ | Decompose (_, [], what, names) ->
+ sprintf "decompose %s%s" what (pp_intros_specs (None, names))
+ | Decompose (_, types, what, names) ->
+ let to_ident = function
+ | Ident id -> id
+ | Type _ -> assert false
+ in
+ let types = List.rev_map to_ident types in
+ sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names))
| Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ pp_term_ast 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"
| Repeat (_, tac) -> "repeat " ^ pp_tactical tac
| Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
| Then (_, tac, tacs) ->
- sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
- | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " 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 ~sep tacs =
String.concat sep (List.map pp_tactical tacs)