diff options
| author | Clément Pit-Claudel | 2018-05-17 23:42:01 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | a249f94d00c64157631fe2517d317dd75ebeff88 (patch) | |
| tree | bb5e3f05d6da33555ee5e2f3974f3b7c9ec553b7 | |
| parent | 468815006f1c272a6ada7186186f90a6692d2521 (diff) | |
[doc] Add a warning about overusing the `coqtop` directive
| -rw-r--r-- | doc/sphinx/README.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 33 |
2 files changed, 66 insertions, 0 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index fbf94fd7da..2884f70477 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -375,6 +375,39 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DONT + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 4ca5171166..d1052d48b2 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -153,6 +153,39 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DONT + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + Tips and tricks =============== |