diff options
| author | Théo Zimmermann | 2019-10-28 10:47:42 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-28 10:47:42 +0100 |
| commit | 342db66cc94a6010a6f301071d251aa458e21547 (patch) | |
| tree | 2f2fd6a4fa0903e033041a0304ff166b0580272e | |
| parent | a8c6c554a0fa282a1e66203bc0c7f76a41054166 (diff) | |
Add changelog for #10963.
| -rw-r--r-- | doc/changelog/03-notations/10963-simplify-parser.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst new file mode 100644 index 0000000000..8b501aac82 --- /dev/null +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -0,0 +1,6 @@ +- A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level stritcly between 100 and 200 and use these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). |