Added ntry and nassumption tactics

[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 7d8c15068bf67c7985ed37846356edbeceaa77ed..95cf5c26f8c4c0e54bec5b8970bd55f89bc67359 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -20,11 +20,13 @@ val merge_tac: NTacStatus.tactic
 val focus_tac: int list -> NTacStatus.tactic
 val unfocus_tac: NTacStatus.tactic
 val skip_tac: NTacStatus.tactic
+val try_tac: NTacStatus.tactic -> NTacStatus.tactic
 
 val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
 val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
 
 val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
+val assumption_tac: NTacStatus.tactic
 val change_tac: 
    where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term -> 
      NTacStatus.tactic