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.Assumption _ -> Tactics.assumption
| GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
MatitaTacticals.solve_tactics
~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
- | GrafiteAst.Skip loc -> MatitaTacticals.skip
- | GrafiteAst.Dot loc -> MatitaTacticals.dot
- | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
- | GrafiteAst.Branch loc -> MatitaTacticals.branch
- | GrafiteAst.Shift loc -> MatitaTacticals.shift
- | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
- | GrafiteAst.Merge loc -> MatitaTacticals.merge
- | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
- | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
in
let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
let status = (* is proof completed? *)