Library Coq.micromega.Zify
Require
Import
ZifyClasses
ZifyInst
.
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
.