X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=0605b993ff125785f7b121a4f3ce2b89cfa4ff5a;hb=ee242468b221c64b25c99b52110fe00380f4eebe;hp=0b805d22bdbc40f7e1b43bcdb58909835843e3da;hpb=d58b48162ad53fb369d285e60a99f746a497ad89;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 0b805d22b..0605b993f 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -40,3 +40,12 @@ val rewrite_tac:
   dir:[ `LeftToRight | `RightToLeft ] ->
    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 ] ->
+      where:NTacStatus.tactic_pattern -> NTacStatus.tactic
+val letin_tac: 
+      where:NTacStatus.tactic_pattern ->
+      what: NTacStatus.tactic_term ->
+      string -> NTacStatus.tactic
+