diff options
| author | Hugo Herbelin | 2020-10-09 17:32:12 +0000 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-16 01:29:19 +0200 |
| commit | 259471cd64cc12d849b0b583c141d2a7041171ab (patch) | |
| tree | 1e083eab189a5b960a76ec9e1229cef015a04ad0 /doc | |
| parent | 0f403373e6ecc1be806b9c29812f5c9f48c321de (diff) | |
Add change log for #13166.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst new file mode 100644 index 0000000000..006989e6b3 --- /dev/null +++ b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). |