]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_tactics/nTactics.mli
instance fixed
[helm.git] / helm / software / components / ng_tactics / nTactics.mli
index 8211adb37ca6c26e91e76716811f826de7ca0e0f..b8659c3574fe63dfb34a170f052e2649408bc70f 100644 (file)
@@ -59,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