tactic cases works! delift clears tags

[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 fffcad698339e0ebd885e52ddf312f92e69b54a3..a834c4e52a8439ac1fea0eda294ad9435c8c5fa2 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -32,5 +32,8 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      NTacStatus.tactic
 val intro_tac: string -> NTacStatus.tactic
+val cases_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     NTacStatus.tactic
 val case1_tac: string -> NTacStatus.tactic