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
---
 Makefile.common | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index dd23d7dd2f..2d1200c071 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -155,13 +155,14 @@ LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
+ZIFYCMO:=plugins/micromega/zify_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO) $(ZIFYCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
-- 
cgit v1.2.3