added tentative elim

[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 0ce7b427eb24c1fdeb3b8fc9dc4dec0cb133cb0a..6c318798e18dc7c90fc87693c57582e23c5737c0 100644 (file)
--- 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