diff options
| author | Pierre-Marie Pédrot | 2021-03-30 16:35:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-30 21:46:12 +0200 |
| commit | 75fec5716327beb1e93f294b70d563300d8f81ec (patch) | |
| tree | 4e3e7ce7326f059181c599621d973214bae7f39d /doc | |
| parent | 6effcc263beded0d530d724fab8edae86815adf8 (diff) | |
Properly expand projection parameters in Btermdn.
The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.
We fix this by adding dummy parameter arguments on sight.
Fixes #14009: TC search failure with primitive projections.
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). |