Library Coq.micromega.Zify


Require Import ZifyClasses ZifyInst.

zify_pre_hook and zify_post_hook are there to be redefined.
Ltac zify_pre_hook := idtac.

Ltac zify_post_hook := idtac.

Ltac iter_specs := zify_iter_specs.

Ltac zify := intros;
             zify_pre_hook ;
             zify_elim_let ;
             zify_op ;
             (zify_iter_specs) ;
             zify_saturate ; zify_post_hook.