| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
- | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm
+ | 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)
~pattern what