X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=7d8c15068bf67c7985ed37846356edbeceaa77ed;hb=635b26d680f72e1ff98d509e7331971e085f9667;hp=3e13035eb792d4188a976d88137f9fe0989a2b36;hpb=a9c8d96d47a5895c99bca2fe93decf464bca62c3;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 3e13035eb..7d8c15068 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -51,3 +51,7 @@ val letin_tac:
 val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   NTacStatus.tactic
+
+val auto_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   NTacStatus.tactic