GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
- idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
- let types = match types with None -> [] | Some types -> types in
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
- let to_spec id = GrafiteAst.Ident id in
- GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+ GrafiteAst.Decompose (loc, idents)
| 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 ->