New debugging tactic nassert:

[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 cc79e05b9486408a6071f45ea0c1cf7738ddebfc..4c3e4d159fda1da9163b3edc711ce252d07ddbf1 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -41,3 +41,13 @@ 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 ] ->
+      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 ->
+  NTacStatus.tactic