Skip to content

Port HeapLang tactics to efficient style

Tej Chajed requested to merge tchajed/iris-coq:efficient-heaplang-tactics into master

Fixes #315 (closed) by porting all of the HeapLang tactics to a style that minimizes the number of environment parameters. This changes the implementations of wp_alloc, wp_load, wp_store, wp_free, wp_cmpxchg, wp_cmpxchg_suc, and wp_faa; there are other tactics but those don't have environments that can be removed.

Edited by Tej Chajed

Merge request reports