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