diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_static/ansi.css | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 2a618f68d2..a4850a738b 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -69,7 +69,7 @@ } .ansi-fg-white { - color: #2e3436; + color: #ffffff; } .ansi-fg-light-black { diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -467,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` |