• Robbert Krebbers's avatar
    Solve atomic also using reification/vm_compute. · 2966b4da
    Robbert Krebbers authored
    I also reverted 7952bca4 since there is no need for atomic to be a
    boolean predicate anymore. Moreover, I introduced a hint database
    fsaV for solving side-conditions related to FSAs, in particular,
    side-conditions related to expressions being atomic.
    2966b4da
Name
Last commit
Last update
..
lib Loading commit data...
derived.v Loading commit data...
heap.v Loading commit data...
lang.v Loading commit data...
lifting.v Loading commit data...
notation.v Loading commit data...
proofmode.v Loading commit data...
tactics.v Loading commit data...
wp_tactics.v Loading commit data...