NTactics.elim_tac
~what:(text,prefix_len,what)
~where:(text,prefix_len,where)
- | GrafiteAst.NEval (_loc, where, reduction) ->
- NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
| GrafiteAst.NGeneralize (_loc, where) ->
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NLetIn (_loc,where,what,name) ->
NTactics.letin_tac ~where:(text,prefix_len,where)
~what:(text,prefix_len,what) name
+ | GrafiteAst.NReduce (_loc, reduction, where) ->
+ NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
| GrafiteAst.NRewrite (_loc,dir,what,where) ->
NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
~where:(text,prefix_len,where)