match ast with
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
- | GrafiteAst.ApplyS (_, term) ->
- Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
+ | GrafiteAst.ApplyS (_, term, params) ->
+ Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
| GrafiteAst.Assumption _ -> Tactics.assumption
| GrafiteAst.Auto (_,params) ->
AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())