diff options
| -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 =============== |