instance fixed

[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 9afd918ead8c2fea14aab2e2a9108a6ad156a84e..b8659c3574fe63dfb34a170f052e2649408bc70f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -15,6 +15,7 @@ val dot_tac: 's NTacStatus.tactic
 val branch_tac: 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
 val pos_tac: int list -> 's NTacStatus.tactic
+val case_tac: string -> 's NTacStatus.tactic
 val wildcard_tac: 's NTacStatus.tactic
 val merge_tac: 's NTacStatus.tactic
 val focus_tac: int list -> 's NTacStatus.tactic
@@ -58,9 +59,5 @@ val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   's NTacStatus.tactic
 
-val auto_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
-   's NTacStatus.tactic
-
 val constructor_tac : 
         ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic