Forked from
Iris / Iris
6381 commits behind the upstream repository.
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.
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| classes.v | ||
| coq_tactics.v | ||
| environments.v | ||
| ghost_ownership.v | ||
| intro_patterns.v | ||
| invariants.v | ||
| notation.v | ||
| pviewshifts.v | ||
| spec_patterns.v | ||
| sts.v | ||
| tactics.v | ||
| weakestpre.v | ||