Coq PR coq/coq#18921 fixes two bugs in the inference of the return clause for Program-style pattern-matching and this has the apparent consequence of modifying the return clause of the match in the definition PCUICSafeChecker.check_projections, and that one more obligation is solved automatically.
We drop the now useless proof (with a comment to indicate that it depends on the Coq version).
To be merged synchronously (though maybe there is a way to make it compatible over different versions? maybe with a Fail?)
Coq PR coq/coq#18921 fixes two bugs in the inference of the return clause for Program-style pattern-matching and this has the apparent consequence of modifying the return clause of the
matchin the definitionPCUICSafeChecker.check_projections, and that one more obligation is solved automatically.We drop the now useless proof (with a comment to indicate that it depends on the Coq version).
To be merged synchronously (though maybe there is a way to make it compatible over different versions?
maybe with a)Fail?