aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proofs
diff options
context:
space:
mode:
authorThéo Zimmermann2020-11-05 14:26:30 +0100
committerThéo Zimmermann2020-11-05 14:26:30 +0100
commit892cb357d89d59dfbb9473885c4e9ec255568ad0 (patch)
tree05d42d05ed89ebc5af66f2b9f4a729c98bb30712 /doc/sphinx/proofs
parent4130c6707497f7fcec7cc1afc363190ada5f2962 (diff)
Improve title of first proof chapter.
Diffstat (limited to 'doc/sphinx/proofs')
-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