aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/ltac.rst3
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst1
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst2
-rw-r--r--doc/sphinx/proof-engine/tactics.rst3
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst3
5 files changed, 0 insertions, 12 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 1fc267488c..38fdf243fe 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
.. _ltac:
The tactic language
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b1e769c571..53294bf8da 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -1,4 +1,3 @@
-.. include:: ../replaces.rst
.. _proofhandling:
-------------------
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 8656e5eb3e..361b6e44a5 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
.. _thessreflectprooflanguage:
------------------------------
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fb121c82ec..b0b57d00a0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
.. _tactics:
Tactics
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 584193b9c6..56df535d85 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
.. _vernacularcommands:
Vernacular commands