| BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
| BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
-let out = ref ignore
-
-let set_callback f = out := f
-
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
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 ->
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
- !out scom;
let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file