Skip to content

Testcase for stdpp!123.

Robbert Krebbers requested to merge robbert/TCEq_hint into master

I discovered this bug while fixing a regression in lambdarust/weak.

The lambdarust problem is also related to https://github.com/coq/coq/issues/11799, but the current testcase really needs the more relaxed modes for TCEq, even if the aforementioned Coq bug is fixed.

This MR needs stdpp!123 (merged)

Merge request reports