From a5aee12a54f02e84dfc36609f3a61bee36073a39 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 5 Nov 2020 11:46:30 +0100
Subject: Add new page to writing proof index.

---
 doc/sphinx/proofs/writing-proofs/index.rst     | 1 +
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index 3f5526dba8..ebd75ef300 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -29,6 +29,7 @@ flavors of tactics, including the SSReflect proof language.
 
    ../../proof-engine/proof-handling
    ../../proof-engine/tactics
+    rewriting
    ../../proof-engine/ssreflect-proof-language
    ../../proof-engine/detailed-tactic-examples
    ../../user-extensions/proof-schemes
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 411eddff42..040849a9ef 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -1,3 +1,7 @@
+=================================
+Term rewriting and simplification
+=================================
+
 .. _rewritingexpressions:
 
 Rewriting expressions
-- 
cgit v1.2.3