X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=fbebd4cbbfc9bc8661d6a89d7d5dfcb0407c1197;hb=5fa31e43ffe25aa7b1539653b137968b5cf9899a;hp=de8c24738b1e3d177073961a7672f16e9532ac89;hpb=dee331ab42d5d625f32fecc3e70df013c2dd093d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index de8c24738..fbebd4cbb 100644
--- 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