From a63bc54bfd697e76182044a8515818fa8f92e849 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Wed, 16 May 2018 21:24:47 -0400
Subject: [doc] Fix a few LaTeX mistakes

---
 doc/sphinx/practical-tools/coqide.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/practical-tools')

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
-- 
cgit v1.2.3


From b3dadd37aa1a9ca8c6be377edb46832b4f3b7256 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 17 May 2018 20:56:04 -0400
Subject: [doc] Include the rst and LaTeX preambles automatically in all files

---
 doc/sphinx/practical-tools/coq-commands.rst | 2 --
 doc/sphinx/practical-tools/coqide.rst       | 2 --
 doc/sphinx/practical-tools/utilities.rst    | 2 --
 3 files changed, 6 deletions(-)

(limited to 'doc/sphinx/practical-tools')

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 9498f37c7e..343ca9ed7d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _thecoqcommands:
 
 The |Coq| commands
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index e8fc29dece..9455228e7d 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _coqintegrateddevelopmentenvironment:
 
 |Coq| Integrated Development Environment
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index b9a4d2a7bd..5d300c3d6d 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _utilities:
 
 ---------------------
-- 
cgit v1.2.3