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 --- doc/changelog/04-tactics/09856-zify.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/04-tactics/09856-zify.rst (limited to 'doc/changelog') diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst new file mode 100644 index 0000000000..6b9143c77b --- /dev/null +++ b/doc/changelog/04-tactics/09856-zify.rst @@ -0,0 +1,7 @@ +- Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. + It can also be extended by redefining the tactic ``zify_post_hook``. + (`#9856 `_ fixes + `#8898 `_, + `#7886 `_, + `#9848 `_ and + `#5155 `_, by Frédéric Besson). -- cgit v1.2.3