Skip to content

Use [fill K] in tac_wp_pure

Tej Chajed requested to merge tchajed/iris-coq:fix-wp-pure into master

This is more consistent with other tac_wp tactics for HeapLang and also a tiny bit more efficient, which is good to embody in the basic tactics so derived code follows the same patterns.

The analogous change to GooseLang made Perennial something like 5% faster to compile.

Merge request reports