From a249f94d00c64157631fe2517d317dd75ebeff88 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 23:42:01 -0400 Subject: [doc] Add a warning about overusing the `coqtop` directive --- doc/sphinx/README.rst | 33 +++++++++++++++++++++++++++++++++ doc/sphinx/README.template.rst | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 66 insertions(+) (limited to 'doc') 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 =============== -- cgit v1.2.3