coq/doc/changelog/04-tactics/14033-fix-14009.rst, branch master The formal proof system Properly expand projection parameters in Btermdn. 2021-03-30T19:46:12+00:00 Pierre-Marie Pédrot 2021-03-30T14:35:42+00:00 75fec5716327beb1e93f294b70d563300d8f81ec 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. 
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.