diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 1 |
2 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst new file mode 100644 index 0000000000..fb12c91729 --- /dev/null +++ b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 <https://github.com/coq/coq/pull/13092>`_, + fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 29877e1b32..f8c0e23696 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -86,6 +86,7 @@ Setting properties of a function's arguments the parameter name used in the function definition). Unless `rename` is specified, the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit arguments. `_` can be used to skip over a formal parameter. + The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. `clear implicits` |