aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum/micromega.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/addendum/micromega.rst')
-rw-r--r--doc/sphinx/addendum/micromega.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index fd66de427c..e799677c59 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -38,7 +38,7 @@ The tactics solve propositional formulas parameterized by atomic
arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
The syntax of the formulas is the following:
- .. productionlist:: `F`
+ .. productionlist:: F
F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n