Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,term) -> Tactics.destruct term
- | GrafiteAst.Elim (_, pattern, using, depth, names) ->
+ | GrafiteAst.Elim (_, what, using, pattern, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- pattern
+ ~pattern what
| GrafiteAst.ElimType (_, what, using, depth, names) ->
Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
what