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.