let idents = match idents with None -> [] | Some idents -> idents in
TacticAst.Intros (loc, num, idents)
| [ IDENT "intro" ] ->
- TacticAst.Intros (loc, None, [])
+ TacticAst.Intros (loc, Some 1, [])
| [ IDENT "left" ] -> TacticAst.Left loc
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->