New tactic "case1_tac" that make "intro" followed by case of the first

[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 de8c24738b1e3d177073961a7672f16e9532ac89..fbebd4cbbfc9bc8661d6a89d7d5dfcb0407c1197 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -47,5 +47,6 @@ val apply_tac: tactic_term -> tactic
 val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic
 val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic
 val intro_tac: string -> tactic
+val case1_tac: string -> tactic
 
 val pp_tac_status: tac_status -> unit