X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.mli;h=13a519d70903c5b4eef34c3b4bdca5d08efd1fb1;hb=81e3d11cbb2a7a6498b4b19876bbb5ababc8942b;hp=7a381cbdc3305b463503e67131ba557b1a913bfb;hpb=643d1536708d85272f8685920abb20790ae5e732;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index 7a381cbdc..13a519d70 100644
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -16,8 +16,18 @@ val fast_eq_check_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
+val paramod_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
+
+val demod_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
+
+val smart_apply_tac: 
+  NTacStatus.tactic_term -> 's NTacStatus.tactic
+
 val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
-val debug : bool ref