GrafiteAst.Reduce (loc, kind, p)
| IDENT "reflexivity" ->
GrafiteAst.Reflexivity loc
+ | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 ->
+ GrafiteAst.Rename (loc, froms, tos)
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+ xnames = OPT [ "as"; n = ident_list0 -> n ] ->
let (pt,_,_) = p in
if pt <> None then
raise
(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)
| IDENT "right" ->
GrafiteAst.Right loc
| IDENT "ring" ->