[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)

1 files changed, 0 insertions, 0 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b3bcb5b056..046cb067c5 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache