[doc] Add another common mistake to the documentation-writing guide

1 files changed, 31 insertions, 1 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
 ===============