diff options
Diffstat (limited to 'doc/sphinx/README.rst')
| -rw-r--r-- | doc/sphinx/README.rst | 32 |
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 =============== |