Replaced long, bugged implementation of letin-tac with two lines of code :-)

[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 0605b993ff125785f7b121a4f3ce2b89cfa4ff5a..b558b4c9b48cae4e627c2687d265e4c42eff6979 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -48,4 +48,6 @@ val letin_tac:
       where:NTacStatus.tactic_pattern ->
       what: NTacStatus.tactic_term ->
       string -> NTacStatus.tactic
-
+val assert_tac:
+ ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
+  NTacStatus.tactic