Skip to content

Fix compilation with Coq 8.10

Tej Chajedrequested to merge
tchajed/iris:fix-mr-488 into master

Fixes a bug from !488 (merged)

The code was inferring an implicit in some complicated way that works on 8.11+. Apparently ; by eauto in later versions is like ; eauto; done (this solves goals 1 and 3, then 2) while in Coq 8.10 it failed because eauto; done fails in the second goal.

CC @robbertkrebbers and @jung

Merge request reports