| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
~pattern what
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
~pattern what