aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
diff options
context:
space:
mode:
authorClément Pit-Claudel2018-05-17 20:56:04 -0400
committerThéo Zimmermann2018-09-20 10:12:55 +0200
commitb3dadd37aa1a9ca8c6be377edb46832b4f3b7256 (patch)
tree5bf7112513d0f09239dfeb70c73c432d20d67100 /doc/sphinx/practical-tools
parent4217ddb700d998e4b57d5e8485380ef9cc16db13 (diff)
[doc] Include the rst and LaTeX preambles automatically in all files
Diffstat (limited to 'doc/sphinx/practical-tools')
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst2
-rw-r--r--doc/sphinx/practical-tools/coqide.rst2
-rw-r--r--doc/sphinx/practical-tools/utilities.rst2
3 files changed, 0 insertions, 6 deletions
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:
---------------------