7 files changed, 7 insertions, 7 deletions
diff --git a/.gitignore b/.gitignore
index 582a8f43c7..0ab6e25852 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,7 +101,7 @@ doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
 doc/sphinx/zebibliography.rst
-doc/sphinx/credits-wrapper.rst
+doc/sphinx/credits.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst
index 212f0a65b0..212f0a65b0 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits-contents.rst
diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst
deleted file mode 100644
index 9f7dd49af8..0000000000
--- a/doc/sphinx/credits-wrapper.latex.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-.. _credits:
-
-.. include:: credits.rst
diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst
index 2d35a12dc2..0b2b1c6ad1 100644
--- a/doc/sphinx/credits-wrapper.html.rst
+++ b/doc/sphinx/credits.html.rst
@@ -4,4 +4,4 @@
 Credits
 -------
 
-.. include:: credits.rst
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst
new file mode 100644
index 0000000000..39101f9d52
--- /dev/null
+++ b/doc/sphinx/credits.latex.rst
@@ -0,0 +1,3 @@
+.. _credits:
+
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 9d90857061..da129a3ed0 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -28,7 +28,7 @@ Table of contents
    :caption: Preamble
 
    self
-   credits-wrapper
+   credits
 
 .. toctree::
    :caption: The language
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 0f2f7b4897..13bc1a19e7 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -10,7 +10,7 @@ Introduction
 Credits
 -------
 
-.. include:: credits-wrapper.rst
+.. include:: credits.rst
 
 License
 -------