[zify] efficiency improvements

- zify_iter_specs is entirely in OCaml
- zify_op has been improved
  * The generation of proof-terms is more direct
  * It does not `rewrite` but instead either performs
    a `pose proof` or a `change`
  * The support for `and`, `or`, `not`, arrow is hardcoded
  * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)

[micromega] fix stack overflow

Less naive computation of bounds (online elimination of duplicates)

0 files changed, 0 insertions, 0 deletions