| 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)