From 921a56a0500651323db9541dea9d195d84776fd2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 30 Aug 2020 15:48:04 -0400
Subject: Fix rendering of -> in micromega

---
 doc/sphinx/addendum/micromega.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index c01e6a5aa6..d7e4c9c804 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -159,7 +159,7 @@ High level view of `lia`
 Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof
 principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually,
 *positivstellensatz* refutations are not even sufficient to decide
-linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}`
+linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 \to \mathtt{False}`
 which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this
 weakness, the :tacn:`lia` tactic is using recursively a combination of:
 
-- 
cgit v1.2.3