X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteParser.ml;h=5b9cea37a8cf9aac01fd186e7b214cd25735af3b;hb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;hp=aa60c87c43267e823461716190a859050117c26b;hpb=b92a0ec32215eea5e0452154da54d5a29a84a53e;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index aa60c87c4..5b9cea37a 100644
--- 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;