let idents = match idents with None -> [] | Some idents -> idents in
return_tactic loc (TacticAst.Intros (num, idents))
| [ IDENT "intro" | IDENT "Intro" ] ->
- return_tactic loc (TacticAst.Intros (Some 1, []))
+ return_tactic loc (TacticAst.Intros (None, []))
| [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->
[ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
| "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
- return_tactical loc (TacticAst.Seq tactics)
+ (match tactics with
+ | [tactic] -> tactic
+ | _ -> return_tactical loc (TacticAst.Seq tactics))
]
| "then" NONA
[ tac = tactical;