diff options
| author | coqbot-app[bot] | 2021-03-31 09:33:00 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-31 09:33:00 +0000 |
| commit | 3442bfa0e7c7e5ba3ce7d62f16d221c2e6da03cf (patch) | |
| tree | b5568e48e853b9c5893aa17f774cecd18421bc6c /doc | |
| parent | 6b5102bad5a75ede001908709f0b159127887667 (diff) | |
| parent | 75fec5716327beb1e93f294b70d563300d8f81ec (diff) | |
Merge PR #14033: Properly expand projection parameters in Btermdn.
Reviewed-by: mattam82
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/14033-fix-14009.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst new file mode 100644 index 0000000000..3b58e193cb --- /dev/null +++ b/doc/changelog/04-tactics/14033-fix-14009.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Properly expand projection parameters in hint discrimination + nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_, + fixes `#9000 <https://github.com/coq/coq/issues/9000>`_, + `#14009 <https://github.com/coq/coq/issues/14009>`_, + by Pierre-Marie Pédrot). |