• Robbert Krebbers's avatar
    Let stateful tactics try all decompositions. · 284ccdd5
    Robbert Krebbers authored
    This problem has been reported by Léon Gondelman.
    
    Before, when using, for example wp_alloc, in an expression like:
    
      ref (ref v)
    
    It would apply `tac_wp_alloc` to the outermost ref, after which it
    fails to establish that the argument `ref v` is a value. In this
    commit, other evaluation positions will be tried whenever it turn
    out that the argument of the construct is not a value. The same
    applies to store/cas/...
    
    I have implemented this by making use of the new `IntoVal` class.
    284ccdd5
proofmode.v 8.44 KB