X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=142300cc0bb91d30d74ef1381adb53fe0678f02f;hb=a3ee89dab26307ce1cedc8041ede995a97d51446;hp=b558b4c9b48cae4e627c2687d265e4c42eff6979;hpb=79659e9015f1f7079b1e7ef846288de60019093a;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index b558b4c9b..142300cc0 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -41,8 +41,8 @@ val rewrite_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
     NTacStatus.tactic
 val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
-val eval_tac: 
-      reduction:[ `Whd of bool ] ->
+val reduce_tac: 
+      reduction:[ `Normalize of bool | `Whd of bool ] ->
       where:NTacStatus.tactic_pattern -> NTacStatus.tactic
 val letin_tac: 
       where:NTacStatus.tactic_pattern ->
@@ -51,3 +51,6 @@ 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:'a -> NTacStatus.tactic