| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
- | IDENT "elim"; what = tactic_term; using = using;
- (num, idents) = intros_spec ->
- GrafiteAst.Elim (loc, what, using, num, idents)
+ | IDENT "elim"; what = tactic_term; using = using;
+ pattern = OPT pattern_spec;
+ (num, idents) = intros_spec ->
+ let pattern = match pattern with
+ | None -> None, [], Some Ast.UserInput
+ | Some pattern -> pattern
+ in
+ GrafiteAst.Elim (loc, what, using, pattern, num, idents)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, num, idents)
| BYC_weproved (ty,id,t1) ->
GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
| BYC_letsuchthat (id1,t1,id2,t2) ->
- (match t with
+ (* (match t with
LNone floc ->
raise (HExtlib.Localized
(floc,CicNotationParser.Parse_error
"tactic_term expected here"))
- | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+ | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
| BYC_wehaveand (id1,t1,id2,t2) ->
(match t with
LNone floc ->