| IDENT "elim"; IDENT "type"; t = tactic_term ->
return_tactic loc (TacticAst.ElimType t)
| IDENT "elim"; t1 = tactic_term;
- using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+ using = OPT [ "using"; using = tactic_term -> using ] ->
return_tactic loc (TacticAst.Elim (t1, using))
| IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
| IDENT "exists" -> return_tactic loc TacticAst.Exists