| [ IDENT "intro" ] ->
TacticAst.Intros (loc, Some 1, [])
| [ IDENT "left" ] -> TacticAst.Left loc
- | [ "let" | "Let" ];
- t = tactic_term; "in"; where = IDENT ->
+ | [ IDENT "letin" ];
+ where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
| kind = reduction_kind;
pat = OPT [