Forked from
Iris / Iris
5003 commits behind the upstream repository.
Jacques-Henri Jourdan
authored
(□ P) now means (bi_bare (bi_persistently P)). This is motivated by the fact that these two modalities are rarely used separately. In the case of an affine BI, we keep the □ notation. This means that a bi_bare is inserted each time we use □. Hence, a few adaptations need to be done in the proof mode class instances.
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| class_instances.v | ||
| classes.v | ||
| coq_tactics.v | ||
| environments.v | ||
| intro_patterns.v | ||
| notation.v | ||
| sel_patterns.v | ||
| spec_patterns.v | ||
| strings.v | ||
| tactics.v | ||
| tokens.v | ||