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)
+ to_what = OPT [ "to" ; t = tactic_term -> t ];
+ ident = OPT [ "using" ; id = IDENT -> id ] ->
+ TacticAst.LApply (loc, to_what, what, ident)
| IDENT "left" -> TacticAst.Left loc
| IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
| IdTac of loc
| Injection of loc * 'term
| Intros of loc * int option * 'ident list
- | LApply of loc * 'term option * 'term
+ | LApply of loc * 'term option * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
| Reduce of loc * reduction_kind * ('term, 'ident) pattern
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
| FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term)
- | LApply (_, term_opt, term) ->
- sprintf "lapply %s%s" (pp_term_ast term)
- (match term_opt with | None -> "" | Some t -> " to " ^ pp_term_ast t)
+ | LApply (_, term_opt, term, ident) ->
+ sprintf "lapply %s%s%s" (pp_term_ast term)
+ (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t)
+ (match ident with None -> "" | Some id -> " " ^ id)
let pp_flavour = function
| `Definition -> "Definition"