Added syntax for ninversion tactic (still experimental).

[helm.git] / helm / software / components / ng_tactics / nTactics.mli

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 74bbcbcb4214a3565506a04d1dc81695bf746970..e1a5de8957735d52ea20863a38c8e54ee080e40f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -95,3 +95,7 @@ val analyze_indty_tac :
 
 
 val find_in_context : 'a -> ('a * 'b) list -> int
+
+val inversion_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     's NTacStatus.tactic