From 97bec684eb514700879778c0da9b05e4264a99f6 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 6 Jan 2020 11:57:11 +0100
Subject: [micromega] fix of bug #11191

- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.
---
 doc/changelog/04-tactics/11362-micromega-fix-11191.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/04-tactics/11362-micromega-fix-11191.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
new file mode 100644
index 0000000000..5ecd46bced
--- /dev/null
+++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Regression of ``lia`` due to more powerful ``zify``
+  (`#11362 <https://github.com/coq/coq/pull/11362>`_,
+  fixes `#11191 <https://github.com/coq/coq/issues/11191>`_,
+  by Frédéric Besson).
-- 
cgit v1.2.3