| Cut of name * what * note
| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
- | Elim of what * using option * note
+ | Elim of what * using option * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| ClearBody of name * note
let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
mk_tactic tactic
-let mk_elim what using =
- let tactic = G.Elim (floc, what, using, Some 0, []) in
+let mk_elim what using pattern =
+ let pattern = None, [], Some pattern in
+ let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
mk_tactic tactic
let mk_apply t =
| Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
| LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
| Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a)
- | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
+ | Elim (t, xu, e, s) -> mk_note s :: cont sep (mk_elim t xu e :: a)
| Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
| Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a)
| ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a)