From dfff69ef604e02703575cb1cb15b2f77eda5f0f4 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 28 Mar 2019 15:24:33 +0100
Subject: Re-implementation of zify

The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress.  If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.

This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.

The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.)  efficiency impact.

There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite
---
 test-suite/success/Nia.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 62ecece792..2eac9660b4 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,8 @@ Open Scope Z_scope.
 
 (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations.
+Require  Zify.
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3