From 3603a6d3324aa54c385f3f84a9fb4d5b9c2fde57 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 10 May 2019 00:15:23 +0200
Subject: Better title for the first example of the Ltac examples section.

---
 doc/sphinx/proof-engine/ltac.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 83b8bc2308..a7eb7c2319 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1179,10 +1179,10 @@ Printing |Ltac| tactics
 Examples of using |Ltac|
 -------------------------
 
-About the cardinality of the set of natural numbers
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Proof that the natural numbers have at least two elements
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. example:: About the cardinality of the set of natural numbers
+.. example:: Proof that the natural numbers have at least two elements
 
    The first example shows how to use pattern matching over the proof
    context to prove that natural numbers have at least two
-- 
cgit v1.2.3