Merge PR #10765: Improved handling of micromega caches

Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl

2 files changed, 15 insertions, 0 deletions

diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst
new file mode 100644
index 0000000000..12d8f68e63
--- /dev/null
+++ b/doc/changelog/04-tactics/10765-micromega-caches.rst
@@ -0,0 +1,3 @@
+- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`.
+  (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case)
+  (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 238106b2e7..4a691bde3a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,18 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. flag:: Lia Cache
+
+   This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
+
+.. flag:: Nia Cache
+
+   This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
+
+.. flag:: Nra Cache
+
+   This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache`
+
 
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.