mk_tactic tactic
let mk_elim what using pattern =
- let pattern = Some what, [], Some pattern in
- let tactic = G.Elim (floc, pattern, using, Some 0, []) in
+ let pattern = None, [], Some pattern in
+ let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
mk_tactic tactic
let mk_apply t =