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
---
 plugins/micromega/plugin_base.dune | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'plugins/micromega/plugin_base.dune')

diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune
index c2d396f0f9..4153d06161 100644
--- a/plugins/micromega/plugin_base.dune
+++ b/plugins/micromega/plugin_base.dune
@@ -2,7 +2,7 @@
  (name micromega_plugin)
  (public_name coq.plugins.micromega)
  ; be careful not to link the executable to the plugin!
- (modules (:standard \ csdpcert))
+ (modules (:standard \ csdpcert g_zify zify))
  (synopsis "Coq's micromega plugin")
  (libraries num coq.plugins.ltac))
 
@@ -13,3 +13,10 @@
  (modules csdpcert)
  (flags :standard -open Micromega_plugin)
  (libraries coq.plugins.micromega))
+
+(library
+ (name zify_plugin)
+ (public_name coq.plugins.zify)
+ (modules g_zify zify)
+ (synopsis "Coq's zify plugin")
+ (libraries coq.plugins.ltac))
-- 
cgit v1.2.3