X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=c492b8c644c1279d2da38b78acd58ffecb4eb338;hb=b6ceb877c05d27705ef163488aee38e60a86886c;hp=5290a322e2db63e79a4209df396ee377e4d70927;hpb=baa054dbb476c30576bf11b81246008a7de53462;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli
index 5290a322e..c492b8c64 100644
--- a/matita/components/ng_tactics/nTactics.mli
+++ b/matita/components/ng_tactics/nTactics.mli
@@ -89,3 +89,5 @@ val find_in_context : 'a -> ('a * 'b) list -> int
 val inversion_tac: 
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
+
+val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic