Skip to content

Fix unexpected implicit binder warning

Tej Chajed requested to merge tchajed/iris-coq:fix-implicit-binder-warning into master

Coq master is stricter about checking for meaningless implicit binders; see https://github.com/coq/coq/pull/10202.

Merge request reports