let mk_rewrite direction what where pattern punctation =
let direction = if direction then `RightToLeft else `LeftToRight in
let pattern, rename = match where with
- | None -> (None, [], Some pattern), []
- | Some (premise, name) -> (None, [premise, pattern], None), [name]
+ | None -> (None, [], Some pattern), []
+ | Some (premise, Some name) -> (None, [premise, pattern], None), [Some name]
+ | Some (premise, None) -> (None, [premise, pattern], None), []
in
let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
mk_tactic tactic punctation
mk_tactic tactic punctation
let mk_apply t punctation =
- let tactic = G.Apply (floc, t) in
+ let tactic = G.ApplyP (floc, t) in
mk_tactic tactic punctation
let mk_change t where pattern punctation =
| p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
render_steps sep (render_step mk_sc a p) ps
| p :: ps ->
- render_steps sep (render_step mk_dot a p) ps
+ render_steps sep (render_step mk_sc a p) ps
let render_steps a = render_steps mk_dot a