diff options
| author | Clément Pit-Claudel | 2018-05-18 01:49:27 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | fdc5e750f7b87c1d0d1454bae19c00eec9dabbeb (patch) | |
| tree | 854a0e0c59c4f67d0a98161fa59c6a7bdbdda4d0 | |
| parent | f39626edcbd56bd7b05aabe8b60e9af72d27bbfd (diff) | |
[doc] Add another common mistake to the documentation-writing guide
| -rw-r--r-- | doc/sphinx/README.rst | 32 | ||||
| -rw-r--r-- | 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 =============== |