Library Coq.micromega.Zify
zify_post_hook is there to be redefined.
Ltac zify_post_hook := idtac.
Ltac iter_specs := zify_iter_specs.
Ltac zify := intros;
zify_elim_let ;
zify_op ;
(zify_iter_specs) ;
zify_saturate ; zify_post_hook.
Ltac iter_specs := zify_iter_specs.
Ltac zify := intros;
zify_elim_let ;
zify_op ;
(zify_iter_specs) ;
zify_saturate ; zify_post_hook.