X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=7be8c816ebb049a87b408bd3fb0ed8e69c47b11f;hb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;hp=617a6d5637abcc3b1111d8f0a7d089bdf47165ab;hpb=b92a0ec32215eea5e0452154da54d5a29a84a53e;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 617a6d563..7be8c816e 100644
--- 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)