New tactic: inversion.

[helm.git] / helm / ocaml / grafite / grafiteAstPp.ml

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 617a6d5637abcc3b1111d8f0a7d089bdf47165ab..7be8c816ebb049a87b408bd3fb0ed8e69c47b11f 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -117,6 +117,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | IdTac _ -> "id"
   | Injection (_, term) -> "injection " ^ term_pp term
   | Intros (_, None, []) -> "intro"
+  | Inversion (_, term) -> "inversion " ^ term_pp term
   | Intros (_, num, idents) ->
       sprintf "intros%s%s"
         (match num with None -> "" | Some num -> " " ^ string_of_int num)