- Add awp_pure to lifting.v - Prove a_load without unfolding awp - Use IntoVal in some rules in monad.v
Dan Frumin authored