[doc] Fix a few LaTeX mistakes

2 files changed, 16 insertions, 12 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ac0f0f8ea6..13d6e228a6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1010,7 +1010,7 @@ the Type hierarchy.
 
    It is possible to declare the same inductive definition in the
    universe :math:`\Type`. The :g:`exType` inductive definition has type
-   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}`
+   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}`
    has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`.
 
    .. coqtop:: all
@@ -1264,14 +1264,14 @@ The |Coq| term for this proof
 will be written:
 
 .. math::
-   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \endkw
+   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend
 
 In this expression, if :math:`m` eventually happens to evaluate to
 :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch
 and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the
 :math:`u_1 … u_{p_i}` according to the ι-reduction.
 
-Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need
+Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need
 to know the predicate P to be proved by case analysis. In the general
 case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
 over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
@@ -1285,7 +1285,7 @@ using the syntax:
 .. math::
    \Match~m~\as~x~\In~I~\_~a~\return~P~\with~
    (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | …
-   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw
+   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
    
 The :math:`\as` part can be omitted if either the result type does not depend
 on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m`
@@ -1471,6 +1471,8 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
    where
 
    .. math::
+      :nowrap:
+
       \begin{eqnarray*}
         P & = & \lambda~l~.~P^\prime\\
         f_1 & = & t_1\\
@@ -1711,13 +1713,15 @@ for primitive recursive operators. The following reductions are now
 possible:
 
 .. math::
-   \def\plus{\mathsf{plus}}
-   \def\tri{\triangleright_\iota}
-   \begin{eqnarray*}
-   \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
-                                  & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
-                                  & \tri & \nS~(\nS~(\nS~\nO))\\
-   \end{eqnarray*}
+   :nowrap:
+
+   {\def\plus{\mathsf{plus}}
+    \def\tri{\triangleright_\iota}
+    \begin{eqnarray*}
+    \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+                                   & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+                                   & \tri & \nS~(\nS~(\nS~\nO))\\
+    \end{eqnarray*}}
 
 .. _Mutual-induction:
 
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index bc6a074a27..e8fc29dece 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -263,7 +263,7 @@ for the ∀ symbol. A list of symbol codes is available at
 An alternative method which does not require to know the hexadecimal
 code of the character is to use an Input Method Editor. On POSIX
 systems (Linux distributions, BSD variants and MacOS X), you can
-use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input
+use `uim` version 1.6 or later which provides a LaTeX-style input
 method.
 
 To configure uim, execute uim-pref-gtk as your regular user. In the