From b389b6e3b6754f9f12190bfd2c0e7f68783b582f Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 20 Jan 2020 15:55:13 +0100
Subject: [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)
---
 test-suite/.csdp.cache | Bin 313112 -> 329899 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b3bcb5b056..046cb067c5 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
-- 
cgit v1.2.3