Added syntax for ninversion tactic (still experimental).

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 239d30d2d1480ff0b0c354a757cacbf4105cc058..783d7e6fc5e624b7dd9d21ebaf9af1c621f95ccd 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -805,6 +805,10 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NInversion (_loc, what, where) ->
+      NTactics.inversion_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
   | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where)