diff options
| author | Théo Zimmermann | 2019-10-28 16:44:45 +0100 |
|---|---|---|
| committer | GitHub | 2019-10-28 16:44:45 +0100 |
| commit | 74c6d69a08b50b77c001ca758d25f1a969bf2c73 (patch) | |
| tree | 91d2079d2b081e73d910a7ef90e48d52ca17cdb9 /doc | |
| parent | 342db66cc94a6010a6f301071d251aa458e21547 (diff) | |
Fix typos.
Co-Authored-By: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/10963-simplify-parser.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst index 8b501aac82..327a39bdb6 100644 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -1,6 +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 + with `constr` at level strictly between 100 and 200 and used 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). |