Merge Requests · Iris

Add support for pure names in intro patterns

iris!400 · opened Mar 23, 2020 by Tej Chajed Iris 3.3
- MERGED
- 3
- 90
updated Apr 17, 2020
Adding a constructor for reflexive transitive closures into bi's

iris!375 · opened Feb 13, 2020 by Jonas Kastberg
- MERGED
- 2
- 39
updated Feb 14, 2020
Add introduction pattern `-# pat` to move a hypothesis to the spatial context

iris!370 · opened Feb 05, 2020 by Robbert
- MERGED
- 2
- 51
updated Feb 18, 2020
add documentation of the global RA pattern

iris!222 · opened Mar 05, 2019 by Ralf Jung
- MERGED
- 2
- 49
updated Mar 13, 2019
Replace unused pattern variables with underscore

stdpp!203 · opened Nov 21, 2020 by Tej Chajed
- MERGED
- 1
- 8
updated Nov 26, 2020
Include fragment in `mnat_auth_auth`

iris!569 · opened Nov 04, 2020 by Robbert
- MERGED
- 1
- 2
updated Nov 05, 2020
Remove dead type classes and notations.

stdpp!197 · opened Oct 28, 2020 by Robbert
- MERGED
- 1
- 5
updated Oct 28, 2020
Strengthen persistent_sep_dup for intuitionistic propositions

iris!556 · opened Oct 28, 2020 by Paolo G. Giarrusso
- MERGED
- 1
- 36
updated Nov 05, 2020
Mapsto notation changes: remove `l ↦ -`, and change `l ↦□ I` to `l ↦_I □`.

iris!555 · opened Oct 27, 2020 by Ralf Jung
- MERGED
- 1
- 19
updated Nov 03, 2020
Improve docs for `iModIntro`.

iris!519 · opened Sep 29, 2020 by Robbert
- MERGED
- 1
- 0
updated Sep 29, 2020
multi-package repositories

iris!514 · opened Sep 26, 2020 by Ralf Jung S-waiting-for-review
- MERGED
- 1
- 31
updated Nov 11, 2020
Isomorphism and validy restriction constructions for cameras.

iris!504 · opened Sep 12, 2020 by Robbert
- MERGED
- 1
- 15
updated Nov 06, 2020
add conversions between functors

iris!498 · opened Sep 07, 2020 by Ralf Jung
- MERGED
- 1
- 15
updated Oct 05, 2020
Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

stdpp!164 · opened Jun 12, 2020 by sarahzrf
- MERGED
- 1
- 10
updated Jun 18, 2020
rename heap_lang modules

iris!452 · opened May 25, 2020 by Ralf Jung
- MERGED
- 1
- 24
updated May 26, 2020
Merge BI and SBI canonical structures 4 of 4 tasks completed

iris!441 · opened May 11, 2020 by Robbert Iris 3.3
- MERGED
- 1
- 87
updated May 25, 2020
Make use of `▷^` notation in its definition.

iris!428 · opened Apr 15, 2020 by Robbert
- MERGED
- 1
- 1
updated Apr 16, 2020
Document `%H` pattern.

iris!423 · opened Apr 07, 2020 by Robbert
- MERGED
- 1
- 18
updated Apr 07, 2020
Logical Relations

actris!3 · opened Apr 02, 2020 by Jonas Kastberg
- MERGED
- 1
- 65
updated Apr 06, 2020
drop_insert -> drop_insert_gt

iris!407 · opened Mar 31, 2020 by Michael Sammler
- MERGED
- 1
- 1
updated Mar 31, 2020