Merge Requests · Iris

Added a new lemma to allocate fragmented ownership in unital gmaps while…

iris!164 · opened Jun 26, 2018 by Jonas Kastberg
- MERGED
- 33
updated Jul 31, 2018
Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more 7 of 7 tasks completed

iris!121 · opened Feb 23, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 35
updated Jul 13, 2018
accessor-style iInv without Hclose

iris!143 · opened Apr 23, 2018 by Ralf Jung gen_proofmode
- MERGED
- 24
updated Jul 13, 2018
Logically atomic triples: Notation, tactics, small example 3 of 3 tasks completed

iris!163 · opened Jun 22, 2018 by Ralf Jung
- MERGED
- 2
updated Jul 13, 2018
Logically atomic stack

examples!9 · opened Jun 18, 2018 by Ralf Jung
- MERGED
- 0
updated Jul 13, 2018
port to gen_proofmode

examples!8 · opened Jun 12, 2018 by Ralf Jung
- MERGED
- 12
updated Jul 13, 2018
Remove plainly_exist_1 from the BI axioms.

iris!95 · opened Dec 04, 2017 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 21
updated Jul 13, 2018
rename valid -> emp_valid

iris!131 · opened Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 15
updated Jul 13, 2018
General Invariant Tactic

iris!116 · opened Feb 16, 2018 by Joseph Tassarotti gen_proofmode
- MERGED
- 81
updated Jul 13, 2018
Proof mode support for monotonous predicates.

iris!100 · opened Dec 11, 2017 by Jacques-Henri Jourdan janno/monfun T-proofmode
- MERGED
- 53
updated Jul 13, 2018
Make `FromPure` depend on an affinity parameter

iris!114 · opened Feb 12, 2018 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 4
updated Jul 13, 2018
BI -> Bi, to match our convention

iris!103 · opened Dec 20, 2017 by Ralf Jung gen_proofmode
- MERGED
- 2
updated Jul 13, 2018
Generalized proofmode

iris!66 · opened Sep 24, 2017 by Robbert Krebbers
- MERGED
- 32
updated Jul 13, 2018
Split prettification from proof mode reduction

iris!170 · opened Jul 04, 2018 by Ralf Jung gen_proofmode
- MERGED
- 4
updated Jul 05, 2018
make `wp_alloc l as "?"` behave as expected

iris!169 · opened Jul 04, 2018 by Ralf Jung gen_proofmode
- MERGED
- 5
updated Jul 04, 2018
Allow comparing even more values in CAS by adding non-determinism

iris!167 · opened Jun 30, 2018 by Ralf Jung gen_proofmode
- MERGED
- 8
updated Jul 03, 2018
Make CAS slightly more realistic

iris!165 · opened Jun 28, 2018 by Ralf Jung gen_proofmode
- MERGED
- 22
updated Jun 30, 2018
Add `Countable` instance for `gset`.

stdpp!40 · opened Jun 29, 2018 by Janno
- MERGED
- 4
updated Jun 29, 2018
begin a test suite

stdpp!39 · opened Jun 25, 2018 by Ralf Jung
- MERGED
- 5
updated Jun 25, 2018
decrease priority for rtc_reflexive instance

stdpp!38 · opened Jun 23, 2018 by Ralf Jung
- MERGED
- 7
updated Jun 25, 2018