aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorHugo Herbelin2020-11-20 10:00:47 +0100
committerGitHub2020-11-20 10:00:47 +0100
commitd13abaf2b7789aecccd607e014025b6c8b9ae094 (patch)
tree87dd9715f0ee609318d4d0cdb23e03d588fb88b2 /doc
parent55389f1a1705b5c548161e1e5cc3eb5e34dda41d (diff)
Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst
index 83baf65526..e63ab9696e 100644
--- a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst
+++ b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst
@@ -1,5 +1,5 @@
- **Fixed:**
- Occasional unexpected capture of the name of global references by
+ Capture of the name of global references by
binders in the presence of notations for binders
(`#12965 <https://github.com/coq/coq/pull/12965>`_,
fixes `#9569 <https://github.com/coq/coq/issues/9569>`_,