let dbd = LibraryDb.instance () in
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.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
- | `Demodulate ->
- GrafiteTypes.command_error "demodulation can't be folded"
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
- | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern