let mk_fresh_name_callback = namer_of names in
Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
| GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
- | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
+ | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
what
Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
| GrafiteAst.Goal (_, n) -> Tactics.set_goal n
| GrafiteAst.IdTac _ -> Tactics.id
- | GrafiteAst.Injection (_,term) -> Tactics.injection term
| GrafiteAst.Intros (_, None, names) ->
PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
| GrafiteAst.Intros (_, Some num, names) ->
| GrafiteAst.Split _
| GrafiteAst.Replace _
| GrafiteAst.Reduce _
- | GrafiteAst.Injection _
| GrafiteAst.IdTac _
| GrafiteAst.Generalize _
| GrafiteAst.Elim _