| GrafiteAst.Decompose (_, names) ->
let mk_fresh_name_callback = namer_of names in
Tactics.decompose ~mk_fresh_name_callback ()
- | GrafiteAst.Demodulate _ ->
+ | GrafiteAst.Demodulate (_, params) ->
Tactics.demodulate
- ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
+ ~dbd:(LibraryDb.instance ()) ~params
+ ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
- | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
| `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
| `Unfold None ->
PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
| `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
| `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)