diff options
| author | coqbot-app[bot] | 2020-12-04 08:29:55 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-04 08:29:55 +0000 |
| commit | b01b5fc9e56cf461d09d2884edefd232c9c63d6e (patch) | |
| tree | 3fe7ec71a6230638dd03bc9f58ded6157e239167 /doc/sphinx/user-extensions | |
| parent | 88f23b3095c223966352b7d8c2d9990250f0c640 (diff) | |
| parent | d20e4edab5912eb41b8408c3c8ab7541f4fc7834 (diff) | |
Merge PR #13527: Changes for Coq 8.13
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index df73de846f..64deb692fd 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -588,6 +588,8 @@ As an exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments (but not of notation scopes). +.. _notations-and-binders: + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ |