- return_tactic loc (TacticAst.Intros (num, idents))
- | [ IDENT "intro" | IDENT "Intro" ] ->
- return_tactic loc (TacticAst.Intros (None, []))
- | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
- | [ "let" | "Let" ];
- t = tactic_term; "in"; where = IDENT ->
- return_tactic loc (TacticAst.LetIn (t, where))
- | kind = reduction_kind;
- pat = OPT [
- "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
- pat
- ];
- terms = LIST0 term SEP SYMBOL "," ->
- let tac =
- (match (pat, terms) with
- | None, [] -> TacticAst.Reduce (kind, None)
- | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
- | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
- in
- return_tactic loc tac
- | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
- return_tactic loc TacticAst.Reflexivity
- | [ IDENT "replace" | IDENT "Replace" ];
- t1 = tactic_term; "with"; t2 = tactic_term ->
- return_tactic loc (TacticAst.Replace (t1, t2))
- (* TODO Rewrite *)
- (* TODO Replace_pattern *)
- | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right
- | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring
- | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split
- | [ IDENT "symmetry" | IDENT "Symmetry" ] ->
- return_tactic loc TacticAst.Symmetry
- | [ IDENT "transitivity" | IDENT "Transitivity" ];
- t = tactic_term ->
- return_tactic loc (TacticAst.Transitivity t)
+ TacticAst.Intros (loc, num, idents)
+ | IDENT "intro"; ident = OPT IDENT ->
+ let idents = match ident with None -> [] | Some id -> [id] in
+ TacticAst.Intros (loc, Some 1, idents)
+ | IDENT "lapply"; what = tactic_term;
+ to_what = OPT [ "to" ; t = tactic_term -> t ] ->
+ TacticAst.LApply (loc, to_what, what)
+ | IDENT "left" -> TacticAst.Left loc
+ | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
+ TacticAst.LetIn (loc, t, where)
+ | kind = reduction_kind; p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Reduce (loc, kind, p)
+ | IDENT "reflexivity" ->
+ TacticAst.Reflexivity loc
+ | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term ->
+ TacticAst.Replace (loc, t1, t2)
+ | IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Rewrite (loc, d, t, p)
+ | IDENT "right" ->
+ TacticAst.Right loc
+ | IDENT "ring" ->
+ TacticAst.Ring loc
+ | IDENT "split" ->
+ TacticAst.Split loc
+ | IDENT "symmetry" ->
+ TacticAst.Symmetry loc
+ | IDENT "transitivity"; t = tactic_term ->
+ TacticAst.Transitivity (loc, t)