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