aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/addendum/micromega.rst6
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index cc19c8b6a9..b0197c500c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,12 @@ 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.
+.. cmd:: Show Lia Profile
+
+ This command prints some statistics about the amount of pivoting
+ operations needed by :tacn:`lia` and may be useful to detect
+ inefficiencies (only meaningful if flag :flag:`Simplex` is set).
+
.. flag:: Lia Cache
This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`