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/stdlib/hidden-files | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

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