From 7d961a914a8eaa889a982a4f84b3ba368d9e8ebc Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 9 Dec 2019 15:28:14 +0100
Subject: [micromega] fix efficiency regression

PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.

Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.

Fixes #11063 and fixes #11242 and fixes #11270
---
 doc/changelog/04-tactics/11263-micromega-fix.rst | 6 ++++++
 doc/stdlib/hidden-files                          | 1 +
 2 files changed, 7 insertions(+)
 create mode 100644 doc/changelog/04-tactics/11263-micromega-fix.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst
new file mode 100644
index 0000000000..ebfb6c19b1
--- /dev/null
+++ b/doc/changelog/04-tactics/11263-micromega-fix.rst
@@ -0,0 +1,6 @@
+- **Fixed**
+  Efficiency regression introduced by  PR `#9725 <https://github.com/coq/coq/pull/9725>`_.
+  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
+  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
+  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
+  and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson).
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index a2bc90ffc0..b816ef6210 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -24,6 +24,7 @@ plugins/extraction/Extraction.v
 plugins/funind/FunInd.v
 plugins/funind/Recdef.v
 plugins/ltac/Ltac.v
+plugins/micromega/Ztac.v
 plugins/micromega/DeclConstant.v
 plugins/micromega/Env.v
 plugins/micromega/EnvRing.v
-- 
cgit v1.2.3