X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=6c318798e18dc7c90fc87693c57582e23c5737c0;hb=780525c2f318cfe782c3d41b70607ba9d72bcc80;hp=0ce7b427eb24c1fdeb3b8fc9dc4dec0cb133cb0a;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 0ce7b427e..6c318798e 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -45,6 +45,7 @@ val block_tac: tactic list -> tactic
 
 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 pp_tac_status: tac_status -> unit