Printf.sprintf "decompose%s"
(pp_intros_specs "names " (None, names))
| Demodulate _ -> "demodulate"
- | Destruct (_, term) -> "destruct " ^ term_pp term
+ | Destruct (_, None) -> "destruct"
+ | Destruct (_, Some term) -> "destruct " ^ term_pp term
| Elim (_, what, using, pattern, specs) ->
Printf.sprintf "elim %s%s %s%s"
(term_pp what)
| Right _ -> "right"
| Ring _ -> "ring"
| Split _ -> "split"
- | Subst _ -> "subst"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)