Merge Requests · Iris

Enable `Typeclasses Strict Resolution` for dervied_connectives.v

iris!641 · opened Feb 19, 2021 by Janno
- CLOSED
- 4
updated Feb 19, 2021
WIP: Remove `contractive_ne` and `contractive_proper` as instances.

iris!455 · opened May 27, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 13
updated Feb 15, 2021
avoid using Hoare triples

examples!43 · opened Dec 12, 2020 by Ralf Jung
- CLOSED
- 1
updated Feb 03, 2021
Fix cast insertion in the front end.

refinedc!17 · opened Jan 23, 2021 by Rodolphe Lepigre
- CLOSED
- 2
updated Jan 28, 2021
Qualify all instances with Local or Global

iris!609 · opened Dec 19, 2020 by Tej Chajed
- CLOSED
- 6
updated Jan 07, 2021
WIP: A library for (monotone) partial bijections.

iris!91 · opened Nov 27, 2017 by Dan Frumin
- CLOSED
- 12
updated Dec 18, 2020
WIP: Avoid inG when possible

iris!219 · opened Feb 20, 2019 by Ralf Jung
- CLOSED
- 23
updated Dec 07, 2020
make wp_apply not call wp_pures

iris!583 · opened Nov 11, 2020 by Ralf Jung
- CLOSED
- 2
updated Dec 04, 2020
Draft: Make sure -#H pattern uses intuitionistic trick

iris!581 · opened Nov 11, 2020 by Tej Chajed
- CLOSED
- 8
updated Nov 27, 2020
WIP: MS-queue

examples!37 · opened Jun 11, 2020 by Simon Friis Vindum
- CLOSED
- 6
updated Nov 26, 2020
WIP: Pretty-print 0 as "0" for N, Z, and nat

stdpp!198 · opened Nov 06, 2020 by Tej Chajed
- CLOSED
- 6
updated Nov 10, 2020
WIP: Documentation on Iris equalities

iris!300 · opened Aug 09, 2019 by Paolo G. Giarrusso S-waiting-for-author
- CLOSED
- 73
updated Nov 06, 2020
Add a way to disable typeclass search in `Program` obligations

stdpp!149 · opened Apr 21, 2020 by Paolo G. Giarrusso
- CLOSED
- 11
updated Nov 03, 2020
Compatibility with Coq PR #12984 regarding new reimports of printing rules.

iris!553 · opened Oct 24, 2020 by Hugo Herbelin
- CLOSED
- 7
updated Oct 29, 2020
WIP: Add persistent points-to predicate to Iris

iris!493 · opened Aug 23, 2020 by Simon Friis Vindum
- CLOSED
- 26
updated Oct 26, 2020
Draft: Drop misleading gmultiset_simple_set instance

stdpp!192 · opened Oct 10, 2020 by Paolo G. Giarrusso
- CLOSED
- 9
updated Oct 12, 2020
Use a smart constructor to build dfrac

iris!534 · opened Oct 06, 2020 by Tej Chajed
- CLOSED
- 1
- 18
updated Oct 09, 2020
Specify how to compile Iris without running the tests

iris!466 · opened Jun 19, 2020 by Dan Frumin S-waiting-for-author
- CLOSED
- 13
updated Sep 30, 2020
Improve framing below modalities

iris!450 · opened May 25, 2020 by Robbert Krebbers S-waiting-for-review
- CLOSED
- 5
updated Sep 29, 2020
WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331

iris!467 · opened Jun 29, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 41
updated Sep 29, 2020