Merge Requests · Iris

Use separate inductives for allocation (refactoring).

refinedc!6 · opened Dec 02, 2020 by Rodolphe Lepigre
- MERGED
- 11
updated Dec 02, 2020
Protocol equivalence

actris!24 · opened Nov 25, 2020 by Jonas Kastberg
- MERGED
- 0
updated Dec 02, 2020
link to pinned-package-versions page

iris!590 · opened Nov 23, 2020 by Ralf Jung
- MERGED
- 1
updated Dec 03, 2020
Add explicit Global to hints at top level

stdpp!202 · opened Nov 20, 2020 by Tej Chajed
- MERGED
- 5
updated Dec 03, 2020
Add explicit Local/Global to hints at top level

iris!594 · opened Nov 27, 2020 by Tej Chajed
- MERGED
- 13
updated Dec 03, 2020
Intptr

refinedc!8 · opened Dec 04, 2020 by Michael Sammler
- MERGED
- 0
updated Dec 04, 2020
Upgrade README demo: it_max -> max_int.

refinedc!9 · opened Dec 04, 2020 by Fengmin Zhu
- MERGED
- 1
updated Dec 04, 2020
add insert_subseteq_l

stdpp!204 · opened Dec 04, 2020 by Ralf Jung
- MERGED
- 3
updated Dec 04, 2020
Make iDestruct consume wands when it's supposed to

iris!591 · opened Nov 25, 2020 by Tej Chajed T-proofmode
- MERGED
- 16
updated Dec 04, 2020
add gmap_view_alloc_big

iris!598 · opened Dec 04, 2020 by Ralf Jung
- MERGED
- 5
updated Dec 04, 2020
wp_finish: avoid making a goal unprovable

iris!593 · opened Nov 26, 2020 by Ralf Jung
- MERGED
- 25
updated Dec 05, 2020
Use user-supplied names when destructing existentials with ? intro pattern

iris!479 · opened Jul 18, 2020 by Tej Chajed
- MERGED
- 64
updated Dec 05, 2020
Remove `CopyDestruct` heuristic

iris!596 · opened Dec 02, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 19
updated Dec 06, 2020
Rename `mnat`/`mnat_auth` into `mono_nat`.

iris!572 · opened Nov 05, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 40
updated Dec 06, 2020
Add support for macros

refinedc!7 · opened Dec 02, 2020 by Michael Sammler
- MERGED
- 6
updated Dec 07, 2020
mono_nat_update: make first argument implicit

iris!600 · opened Dec 07, 2020 by Ralf Jung
- MERGED
- 1
updated Dec 07, 2020
Add missing `Hint Mode` for `ghost_var` and `gset_bij`; fix arguments of `gset_bijG`

iris!601 · opened Dec 07, 2020 by Robbert Krebbers
- MERGED
- 1
updated Dec 07, 2020
Adding rules for intptr casts.

refinedc!10 · opened Dec 07, 2020 by Rodolphe Lepigre
- MERGED
- 3
updated Dec 09, 2020
adjust notation for step-taking updates

iris!462 · opened Jun 15, 2020 by Ralf Jung Iris 3.3
- MERGED
- 24
updated Dec 10, 2020
Ensure variable names do not clash with Coq keywords.

refinedc!11 · opened Dec 10, 2020 by Rodolphe Lepigre
- MERGED
- 0
updated Dec 11, 2020