diff options
| author | coqbot-app[bot] | 2021-04-08 15:45:19 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-08 15:45:19 +0000 |
| commit | e4a8b03d94128ccc05dd429756f07247a1f929cc (patch) | |
| tree | a15708e9036506347e2c1772407a85b097f7ad4b /doc/sphinx | |
| parent | 3bff0b42f5549c371872ddaca1ccd1b1b3b4dce5 (diff) | |
| parent | 45e064836ec1f50300198f89c099b71d0e2059b9 (diff) | |
Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular
Reviewed-by: JasonGross
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 1 |
1 files changed, 1 insertions, 0 deletions
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` |