• Dan Frumin's avatar
    Add awp_pure · 3be6384b
    Dan Frumin authored
    - Add awp_pure to lifting.v
    - Prove a_load without unfolding awp
    - Use IntoVal in some rules in monad.v
    3be6384b
_CoqProject 278 Bytes