New tactic: inversion.

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

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index 7b6b69d44479efacd2ecba74b1030e0e465acfa7..e6cc064a5e928ede7333bd4f776378e1abe03c62 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -170,6 +170,9 @@ let disambiguate_tactic status goal tactic =
         let term = disambiguate_term status_ref goal term in
         GrafiteAst.Injection (loc,term)
     | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.Inversion (loc, term) ->
+       let term = disambiguate_term status_ref goal term in
+        GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
        let f term to_what =
           let term = disambiguate_term status_ref goal term in