diff options
| author | Hugo Herbelin | 2020-09-26 10:43:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-19 10:19:17 +0200 |
| commit | 74fc0e6a280bbbf1f367bfbd73f0833b4d7e525f (patch) | |
| tree | 21f8be82d78df767add41449abc419768bc21da4 | |
| parent | 116e82b44946998dad06b33b3fdc2516fca42fcc (diff) | |
Adding change log for #13092.
| -rw-r--r-- | doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst | 5 |
1 files changed, 5 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). |