diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/10765-micromega-caches.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 12 |
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}\}`. |