X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=b558b4c9b48cae4e627c2687d265e4c42eff6979;hb=de9926defa9fdb4aaebbad4f4131b7704602597b;hp=fffcad698339e0ebd885e52ddf312f92e69b54a3;hpb=8f4bb4db3597080b57d957eb444e58e032da2d78;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index fffcad698..b558b4c9b 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -32,5 +32,22 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      NTacStatus.tactic
 val intro_tac: string -> NTacStatus.tactic
+val cases_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     NTacStatus.tactic
 val case1_tac: string -> NTacStatus.tactic
-
+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
+val assert_tac:
+ ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
+  NTacStatus.tactic