Added initial support for inversion principles in Matita NG.

[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 9afd918ead8c2fea14aab2e2a9108a6ad156a84e..8211adb37ca6c26e91e76716811f826de7ca0e0f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -15,6 +15,7 @@ val dot_tac: 's NTacStatus.tactic
 val branch_tac: 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
 val pos_tac: int list -> 's NTacStatus.tactic
+val case_tac: string -> 's NTacStatus.tactic
 val wildcard_tac: 's NTacStatus.tactic
 val merge_tac: 's NTacStatus.tactic
 val focus_tac: int list -> 's NTacStatus.tactic