Merge Requests · Iris

👻 notation for `own`. 0 of 1 task completed

iris!233 · opened Apr 09, 2019 by Robbert Krebbers
- CLOSED
- 5
- 5
updated Apr 23, 2019
Use a smart constructor to build dfrac

iris!534 · opened Oct 06, 2020 by Tej Chajed
- CLOSED
- 1
- 18
updated Oct 09, 2020
Generalize (e)feed pose proof to intro patterns

stdpp!118 · opened Feb 25, 2020 by Paolo G. Giarrusso
- CLOSED
- 1
- 3
updated Mar 05, 2020
WIP: Generic union, disjoint union CMRAs for sets.

iris!381 · opened Feb 23, 2020 by David Swasey S-waiting-for-author
- CLOSED
- 1
- 30
updated Sep 29, 2020
Enable `Typeclasses Strict Resolution` for dervied_connectives.v

iris!641 · opened Feb 19, 2021 by Janno
- CLOSED
- 4
updated Feb 19, 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
avoid using Hoare triples

examples!43 · opened Dec 12, 2020 by Ralf Jung
- CLOSED
- 1
updated Feb 03, 2021
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: 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
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
Draft: Drop misleading gmultiset_simple_set instance

stdpp!192 · opened Oct 10, 2020 by Paolo G. Giarrusso
- CLOSED
- 9
updated Oct 12, 2020
WIP: Prototype a validity restriction CMRA construction

iris!502 · opened Sep 08, 2020 by Tej Chajed S-waiting-for-author
- CLOSED
- 24
updated Sep 14, 2020
fix various uses of generated names

stdpp!181 · opened Aug 29, 2020 by Ralf Jung
- CLOSED
- 3
updated Aug 30, 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
excl_auth: support fractions in authoritative element

iris!487 · opened Aug 10, 2020 by Ralf Jung
- CLOSED
- 5
updated Aug 11, 2020
[simpl_map]: avoid using [rewrite .. by ..]

stdpp!177 · opened Jul 20, 2020 by Armaël Guéneau
- CLOSED
- 4
updated Sep 29, 2020
if instances for absorbing, affine and persistent

iris!474 · opened Jul 13, 2020 by Alix Trieu S-waiting-for-author
- CLOSED
- 8
updated Sep 08, 2020
WIP: use bytes to represent identifiers in the proofmode

iris!473 · opened Jul 12, 2020 by Tej Chajed S-blocked-by-coq
- CLOSED
- 6
updated Sep 07, 2020