diff --git a/CHANGELOG.md b/CHANGELOG.md
index 471a14caa..fae17fa3f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,5 @@
 # New in next version
++ Documentation added to proof section
 
 ## Tool updates
 + Modules no longer require building if imports have changed but all
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index e6b4282df..925abb416 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -143,6 +143,7 @@ Luke Palmer
 Mark Farrell
 Markus Klink
 Markus Pfeiffer
+Martin Baker
 Mathnerd314
 Mattias Lundell
 Matvey B. Aksenov
diff --git a/docs/proofs/index.rst b/docs/proofs/index.rst
index 51d0d4e0c..dc8706531 100644
--- a/docs/proofs/index.rst
+++ b/docs/proofs/index.rst
@@ -18,6 +18,7 @@ A tutorial on theorem proving in Idris.
 .. toctree::
    :maxdepth: 1
 
+   definitional
    pluscomm
    inductive
    patterns