diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 11:59:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:02 +0200 |
| commit | 21c7793a458848e941a0a6edeb216c2076d947e5 (patch) | |
| tree | 9fad9402e63c626fcb142514845cba05e0c4477f /doc/sphinx/addendum | |
| parent | 1ccb800d20f91f1566d59b549a8422f2230c25d5 (diff) | |
[sphinx] Fix some references.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 4f8cc34d4..f887a5fee 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -113,7 +113,7 @@ tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tac:`romega` +This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` tactics. Roughly speaking, the deductive power of lia is the combined deductive power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following |