Fix issue #288: iExists fails if goal after the existential quantifier is an evar (!372) · Merge requests · Iris / Iris

Robbert Krebbers requested to merge ci/robbert/issue288 into master Feb 06, 2020

Issue #288 (closed) is caused by Coq's TC algorithm using the broken unification algorithm. We fix this through a Hint Extern that uses notypeclasses refine.

I don't quite like this fix, but I see no other way.

Edited Feb 10, 2020 by Robbert Krebbers

Fix issue #288: iExists fails if goal after the existential quantifier is an evar

Merge request reports