Skip to content

Fix wp_alloc when applying twp_allocN

Tej Chajed requested to merge tchajed/iris-coq:fix-twp_allocN-tac into master

The bug manifests as wp_alloc l as "H" always resulting in an error l is not fresh (because intros l was failing).

Merge request reports