Adapt w.r.t. coq/coq#17564.
This is backwards compatible.
The current master branch exploits a bug in the intropattern evaluation, where a split pattern is successfully applied to a higher-order hypothesis even though the dependent argument cannot be solved.