From fdc5e750f7b87c1d0d1454bae19c00eec9dabbeb Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 18 May 2018 01:49:27 -0400
Subject: [doc] Add another common mistake to the documentation-writing guide

---
 doc/sphinx/README.rst          | 32 +++++++++++++++++++++++++++++++-
 doc/sphinx/README.template.rst | 32 +++++++++++++++++++++++++++++++-
 2 files changed, 62 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 6d5545ec3c..369a3a0db8 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -419,7 +419,7 @@ DO
 
         first [ t1 | … | tn ].
 
-DONT
+DON'T
   .. code::
 
      A tactic of the form:
@@ -451,6 +451,36 @@ DON'T
 
 Plain quotes produce plain text, without highlighting or cross-references.
 
+Overusing the ``example`` directive
+-----------------------------------
+
+DO
+  .. code::
+
+     Here is a useful axiom:
+
+     .. coqdoc::
+
+        Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
+DO
+  .. code::
+
+     .. example:: Using proof-irrelevance
+
+        If you assume the axiom above, …
+
+DON'T
+  .. code::
+
+     Here is a useful axiom:
+
+     .. example::
+
+        .. coqdoc::
+
+           Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 73b2e96dcb..86914a71df 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -197,7 +197,7 @@ DO
 
         first [ t1 | … | tn ].
 
-DONT
+DON'T
   .. code::
 
      A tactic of the form:
@@ -229,6 +229,36 @@ DON'T
 
 Plain quotes produce plain text, without highlighting or cross-references.
 
+Overusing the ``example`` directive
+-----------------------------------
+
+DO
+  .. code::
+
+     Here is a useful axiom:
+
+     .. coqdoc::
+
+        Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
+DO
+  .. code::
+
+     .. example:: Using proof-irrelevance
+
+        If you assume the axiom above, …
+
+DON'T
+  .. code::
+
+     Here is a useful axiom:
+
+     .. example::
+
+        .. coqdoc::
+
+           Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
 Tips and tricks
 ===============
 
-- 
cgit v1.2.3