diff options
| author | Hugo Herbelin | 2020-11-14 09:32:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-14 09:32:30 +0100 |
| commit | bad1d9a5263d1128541bc669f81ae81173ce45df (patch) | |
| tree | e66f950fa0a92b2ed0b0e8c514de8c3837017184 /doc | |
| parent | c3853226d1325b452f797309fbb8461ee45a64db (diff) | |
Add changelog for #13376.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst new file mode 100644 index 0000000000..5758f35c3d --- /dev/null +++ b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst @@ -0,0 +1,5 @@ +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 <https://github.com/coq/coq/pull/13376>`_, + fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, + by Hugo Herbelin). |