Merge Requests · Iris · GitLab

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
ASCII notation

iris!396 · opened Mar 18, 2020 by Gregory Malecha Iris 3.3
- MERGED
- 154
updated Apr 08, 2020
Fix issue #260: Error message when iLöb used on non-SBI

iris!302 · opened Aug 12, 2019 by Robbert Krebbers Iris 3.2
- MERGED
- 6
updated Aug 13, 2019
Fix issue #259: Error message when iRevert is used on out of scope variable

iris!301 · opened Aug 12, 2019 by Robbert Krebbers Iris 3.2
- MERGED
- 7
updated Aug 13, 2019
Move array stuff to own file

iris!299 · opened Aug 07, 2019 by Ralf Jung Iris 3.2
- MERGED
- 13
updated Aug 13, 2019
fix typo in -d> docs

iris!298 · opened Aug 07, 2019 by Ralf Jung Iris 3.2
- MERGED
- 19
updated Aug 12, 2019
Add `head_prim_fill_reducible`.

iris!293 · opened Jul 12, 2019 by Dan Frumin Iris 3.2
- MERGED
- 4
updated Nov 24, 2020
Add `big_sepL2_app_inv_2`.

iris!292 · opened Jul 12, 2019 by Dan Frumin Iris 3.2
- MERGED
- 9
updated Nov 24, 2020
Add heap_lang lib for "invariant locations": locations with a (pure) invariant attached to them

iris!289 · opened Jul 12, 2019 by Ralf Jung Iris 3.3
- MERGED
- 145
updated Aug 23, 2020
show that pair construction commutes with taking the core

iris!286 · opened Jul 07, 2019 by Ralf Jung Iris 3.2
- MERGED
- 6
updated Nov 24, 2020
Mark projections for sigTO as NonExpansive and Proper

iris!285 · opened Jul 06, 2019 by Paolo G. Giarrusso Iris 3.2
- MERGED
- 15
updated Nov 24, 2020
heap_lang: Make binary "=" operator partial, to sync with CmpXchg

iris!283 · opened Jun 29, 2019 by Ralf Jung Iris 3.2 T-heap_lang
- MERGED
- 9
updated Nov 24, 2020
Replace `C`s with `O`s since we use OFEs instead of COFEs.

iris!263 · opened Jun 11, 2019 by Robbert Krebbers Iris 3.2
- MERGED
- 18
updated Nov 24, 2020
A strong adequacy statement to rule them all

iris!258 · opened Jun 07, 2019 by Robbert Krebbers Iris 3.2
- MERGED
- 45
updated Jun 12, 2019
Add ghost data to locations

iris!249 · opened May 21, 2019 by Robbert Krebbers Iris 3.2
- MERGED
- 73
updated Sep 09, 2020
The unbounded fractional authoritative camera

iris!187 · opened Oct 31, 2018 by Robbert Krebbers Iris 3.2
- MERGED
- 54
updated Jun 22, 2019
move the reduction control of the proofmode to its own file and tweak it

iris!150 · opened May 24, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 67
updated Jun 15, 2018
provide big_op lemmas outside of bi module

iris!149 · opened May 23, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 8
updated May 29, 2018
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)

iris!148 · opened May 23, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 48
updated Jun 05, 2018
more consistent lemma naming

iris!135 · opened Mar 22, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 1
updated Apr 03, 2018

Prev
1
2
3
4
5
6
…
46
Next