huge commit regarding the grafite_status:

[helm.git] / helm / software / components / ng_tactics / nTactics.mli

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index a834c4e52a8439ac1fea0eda294ad9435c8c5fa2..7d8c15068bf67c7985ed37846356edbeceaa77ed 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -36,4 +36,22 @@ 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 reduce_tac: 
+      reduction:[ `Normalize of bool | `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
 
+val auto_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   NTacStatus.tactic