Mentions légales du service

Skip to content

Adapt w.r.t. coq/coq#17564.

Pierre-Marie Pédrot requested to merge pedrot/coquelicot:case-pf-pose-dependent-metas into master

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.

Merge request reports