aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/proofs/writing-proofs/index.rst6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index f46d8f8b72..1c7fd050f1 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -1,8 +1,8 @@
.. _writing-proofs:
-==============
-Writing proofs
-==============
+===================
+Basic proof writing
+===================
|Coq| is an interactive theorem prover, or proof assistant, which means
that proofs can be constructed interactively through a dialog between