New tactic: inversion.

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

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index e1ae5865d43e6ef1dcc0e2de060b46e9636f06e3..810e54140adac17bb5b721d9b7fa6970de575d7a 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -70,6 +70,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | IdTac of loc
   | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
+  | Inversion of loc * 'term
   | LApply of loc * int option * 'term list * 'term * 'ident option
   | Left of loc
   | LetIn of loc * 'term * 'ident