diff options
Diffstat (limited to 'doc')
| -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 =============== |