From e45bada261c42152e0b835cae7e989a7fccc0fb7 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 18 May 2018 00:07:36 -0400
Subject: [doc] Add more common mistakes to the documentation-writing guide

---
 doc/sphinx/README.rst          | 43 ++++++++++++++++++++++++++++++++++++++++++
 doc/sphinx/README.template.rst | 43 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 86 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 2884f70477..6d5545ec3c 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -362,6 +362,32 @@ DON'T
 
      This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
 
+..
+
+DO
+  .. code::
+
+     :n:`power_tac @term [@ltac]`
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+DON'T
+  .. code::
+
+     power_tac :n:`@term` [:n:`@ltac`]
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+..
+
+DO
+  .. code::
+
+     :n:`name={*; attr}`
+
+DON'T
+  .. code::
+
+     ``name=``:n:`{*; attr}`
+
 Omitting annotations
 --------------------
 
@@ -408,6 +434,23 @@ DONT
 
         first [ t1 | … | tn ].
 
+Overusing plain quotes
+----------------------
+
+DO
+  .. code::
+
+     The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception.
+     The term :g:`let a = 1 in a a` is ill-typed.
+
+DON'T
+  .. code::
+
+     The ``refine`` tactic can raise the ``Invalid argument`` exception.
+     The term ``let a = 1 in a a`` is ill-typed.
+
+Plain quotes produce plain text, without highlighting or cross-references.
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index d1052d48b2..73b2e96dcb 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -140,6 +140,32 @@ DON'T
 
      This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
 
+..
+
+DO
+  .. code::
+
+     :n:`power_tac @term [@ltac]`
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+DON'T
+  .. code::
+
+     power_tac :n:`@term` [:n:`@ltac`]
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+..
+
+DO
+  .. code::
+
+     :n:`name={*; attr}`
+
+DON'T
+  .. code::
+
+     ``name=``:n:`{*; attr}`
+
 Omitting annotations
 --------------------
 
@@ -186,6 +212,23 @@ DONT
 
         first [ t1 | … | tn ].
 
+Overusing plain quotes
+----------------------
+
+DO
+  .. code::
+
+     The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception.
+     The term :g:`let a = 1 in a a` is ill-typed.
+
+DON'T
+  .. code::
+
+     The ``refine`` tactic can raise the ``Invalid argument`` exception.
+     The term ``let a = 1 in a a`` is ill-typed.
+
+Plain quotes produce plain text, without highlighting or cross-references.
+
 Tips and tricks
 ===============
 
-- 
cgit v1.2.3