Several improvements and fixes of Lia

- Improved reification for Micromega (support for #8764)

- Fixes #9268: Do not take universes into account in lia reification

  Improve #9291 by threading the evar_map during reification.
  Universes are unified.

- Remove (potentially cyclic) dependency over lra for Rle_abs

- Towards a complete simplex-based lia

  fixes  #9615

Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal  for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.

For scalability, nia is currently NOT performing this pre-processing.

- Lia is using the FSet library

  manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
  to work around a "leaked" hint breaking compatibility of eauto

2 files changed, 3 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7b395900e9..afb0239be4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used.
                       environment, including those used for ``setoid_rewrite``,
                       from the Classes directory.
 
+:fset: internal database for the implementation of the ``FSets`` library.
+
 You are advised not to put your own hints in the core database, but
 use one or several databases specific to your development.
 
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index b58148ffff..b25104ddb9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -22,6 +22,7 @@ plugins/extraction/Extraction.v
 plugins/funind/FunInd.v
 plugins/funind/Recdef.v
 plugins/ltac/Ltac.v
+plugins/micromega/DeclConstant.v
 plugins/micromega/Env.v
 plugins/micromega/EnvRing.v
 plugins/micromega/Fourier.v