• 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
..
classes.v Loading commit data...
coq_tactics.v Loading commit data...
environments.v Loading commit data...
ghost_ownership.v Loading commit data...
intro_patterns.v Loading commit data...
invariants.v Loading commit data...
notation.v Loading commit data...
pviewshifts.v Loading commit data...
spec_patterns.v Loading commit data...
sts.v Loading commit data...
tactics.v Loading commit data...
weakestpre.v Loading commit data...