- Oct 01, 2020
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
put it into a type class `BiPureForall`. This property does not hold for embeddings of classical logic into Coq.
-
- Sep 30, 2020
-
-
Ralf Jung authored
Remove anonymous Type fields from camera structures. See merge request iris/iris!525
-
Robbert Krebbers authored
These were already removed from the OFE and BI structures, but were left here.
-
Robbert Krebbers authored
Lemmas about big op on lists for !485 See merge request iris/iris!509
-
Michael Sammler authored
-
- Sep 29, 2020
-
-
Ralf Jung authored
-
Ralf Jung authored
strengthen uPred_mono See merge request iris/iris!513
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
More general instance for framing under `<affine>` See merge request iris/iris!522
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Make `iFrame` "less" smart w.r.t. clean up of modalities. See merge request iris/iris!521
-
Robbert Krebbers authored
various algebra lemmas See merge request iris/iris!523
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Previously, if would "cleanup" `<affine>` and `□` if the result after framing is affine and intuitionistic, respectively. This behavior was inconsistent, since similar "cleanup" was not performed for `<absorbing>` and `<persistent>`. This MR thus removes this "cleanup" of modalities. It now consistently removes the modalities `<affine>`, `<absorbing>, `<persistent>` and `□` only if the result after framing is `True` or `emp`. Since `iFrame` is already very complicated, and since its performance is sometimes suboptimal in bigger developments, @jung and I believed doing fewer "smart" things is better than the alternative, namely performing doing sophisticated "cleanup" for all modalities, which is presented in iris/iris!450
-
Robbert Krebbers authored
document Iris side-effects Closes #311 See merge request iris/iris!524
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Strengthen auth_both_valid and auth_both_frac_valid See merge request iris/iris!520
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Improve docs for `iModIntro`. See merge request iris/iris!519
-
Robbert Krebbers authored
Based om iris/iris!467 (comment 53064) by @Blaisorblade.
-
Robbert Krebbers authored
Fix typos See merge request iris/iris!518
-
Paolo G. Giarrusso authored
-
- Sep 28, 2020
-
-
Robbert Krebbers authored
Improve some iIntros error messages See merge request iris/iris!517
-
Tej Chajed authored
A failing iIntros for implications should prettify the identifier before printing, and iIntros on something that isn't a wand or implication should say what couldn't be introduced (to clarify that `iIntros "HP HQ"` failed because of the HQ in particular, for example).
-
Ralf Jung authored
ghost-var lib: more lemmas for when you own the two halves See merge request iris/iris!511
-
Ralf Jung authored
-
- Sep 27, 2020
-
-
Ralf Jung authored
Fix direction of `auth_auth_validN` See merge request iris/iris!515
-
Robbert Krebbers authored
-
Robbert Krebbers authored
For example, `auth_auth_valid`.
-
- Sep 26, 2020
-
-
Ralf Jung authored
-
- Sep 24, 2020
-
-
Robbert Krebbers authored
Fix error when destructing as multiple pats See merge request iris/iris!512
-
Tej Chajed authored
`iDestruct H as "H1 H2"` produces an error that says the pattern should contain exactly one proper introduction pattern. When multiple patterns are provided, due to Ltac variable shadowing iDestructHypFindPat was instead reporting only the first pattern in the error message (and even that was printed as the parsed AST rather than the original string).
-