| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NElim (loc, what, where)
| SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NElim (loc, what, where)
| SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
| SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
| SYMBOL "*"; n=IDENT ->
GrafiteAst.NCase1 (loc,n)
| SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
| SYMBOL "*"; n=IDENT ->
GrafiteAst.NCase1 (loc,n)