New tactic: inversion.

[helm.git] / helm / ocaml / grafite_parser / grafiteParser.ml

diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index aa60c87c43267e823461716190a859050117c26b..5b9cea37a8cf9aac01fd186e7b214cd25735af3b 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteParser.ml
+++ b/helm/ocaml/grafite_parser/grafiteParser.ml
@@ -183,6 +183,8 @@ EXTEND
         GrafiteAst.Intros (loc, Some 1, idents)
     | IDENT "intros"; (num, idents) = intros_spec ->
         GrafiteAst.Intros (loc, num, idents)
+    | IDENT "inversion"; t = tactic_term ->
+        GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       what = tactic_term;