GrafiteAst.Assumption loc
| IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
GrafiteAst.Assumption loc
| IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
+ | IDENT "cases"; what = tactic_term;
+ (num, idents) = intros_spec ->
+ GrafiteAst.Cases (loc, what, idents)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
GrafiteAst.Reflexivity loc
GrafiteAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
GrafiteAst.Reflexivity loc
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
(CicNotationParser.Parse_error
"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
else
(CicNotationParser.Parse_error
"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
else
- GrafiteAst.Rewrite (loc, d, t, p)
+ let n = match xnames with None -> [] | Some names -> names in
+ GrafiteAst.Rewrite (loc, d, t, p, n)
| LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
| IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
GrafiteAst.We_need_to_prove (loc, t, id, t1)
| LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
| IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
GrafiteAst.We_need_to_prove (loc, t, id, t1)
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
| IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
| IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->