tactic: [
[ IDENT "absurd"; t = tactic_term ->
GrafiteAst.Absurd (loc, t)
tactic: [
[ IDENT "absurd"; t = tactic_term ->
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
| IDENT "applyP"; t = tactic_term ->
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
| IDENT "applyP"; t = tactic_term ->
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)