Commits · 625011cf7f7c522cfa197958012147cfcb9206a9 · Iris / Iris

30 Jul, 2019 1 commit
- explain weird anonymous type field in CmraT · 625011cf
  Ralf Jung authored Jul 30, 2019
  
  625011cf
22 Jul, 2019 1 commit
- mention how to use iLöb for recursive functions · 8dfda06c
  Ralf Jung authored Jul 22, 2019
  
  8dfda06c
14 Jul, 2019 4 commits
- Merge branch 'big_sepL2_app_inv_2' into 'master' · 0cdad2cb
  Robbert authored Jul 14, 2019
```
Add `big_sepL2_app_inv_2`.

See merge request !292
```
  0cdad2cb
- Rename `big_sepL2_app_inv_2` -> `big_sepL2_app_inv`. · 2a4e4330
  Dan Frumin authored Jul 14, 2019
```
And shorten the proof.
```
  2a4e4330
- Merge branch 'head_prim_fill_reducible' into 'master' · cd8f3be9
  Robbert authored Jul 14, 2019
```
Add `head_prim_fill_reducible`.

See merge request iris/iris!293
```
  cd8f3be9
- Add `head_prim_fill_reducible`. · 4767c8f9
  Dan Frumin authored Jul 14, 2019
```
A more general implication from `head_reducible` to `reducible`.
```
  4767c8f9
13 Jul, 2019 7 commits
- Merge branch 'sigTO_proper_projs' into 'master' · 9b77b750
  Robbert authored Jul 13, 2019
```
Mark projections for sigTO as NonExpansive and Proper

See merge request !285
```
  9b77b750
- Mark projections for sigTO as NonExpansive and Proper · 53a18cf8
  Paolo G. Giarrusso authored Jul 13, 2019
  
  53a18cf8
- proper link and less Rust ;) · 94533e33
  Ralf Jung authored Jul 13, 2019
  
  94533e33
- erasure is in iris/examples · b5e2eb4e
  Ralf Jung authored Jul 13, 2019
  
  b5e2eb4e
- Weaken premise of `gmultiset_local_update_dealloc`. · 736b17dc
  Robbert Krebbers authored Jul 13, 2019
  
  736b17dc
- Merge branch 'ralf/pair-core' into 'master' · 8f41613d
  Robbert authored Jul 13, 2019
```
show that pair construction commutes with taking the core

See merge request !286
```
  8f41613d
- shorten proof · 162755de
  Ralf Jung authored Jul 13, 2019
  
  162755de
12 Jul, 2019 2 commits
- tweak proof to also work after a Coq bugfix · e6f6758c
  Ralf Jung authored Jul 12, 2019
  
  e6f6758c
- changelog for comparison changes · f455b5d4
  Ralf Jung authored Jul 12, 2019
  
  f455b5d4
09 Jul, 2019 4 commits
- dont quantify over empty telescopes · c2eaa77d
  Ralf Jung authored Jul 09, 2019
  
  c2eaa77d
- Merge branch 'fresh_locs_arg' into 'master' · 64c16f99
  Robbert authored Jul 09, 2019
```
Get rid of a superflous argument to `fresh_locs`.

See merge request iris/iris!288
```
  64c16f99
- Get rid of a superflous argument to `fresh_locs`. · 80623a8c
  Dan Frumin authored Jul 09, 2019
  
  80623a8c
- bump std++ · 5123ac6b
  Ralf Jung authored Jul 09, 2019
  
  5123ac6b
07 Jul, 2019 1 commit
- show that pair cosntruction commutes with taking the core · c2d34fe3
  Ralf Jung authored Jul 07, 2019
  
  c2d34fe3
05 Jul, 2019 2 commits
- Bump stdpp. · 4a624063
  Robbert Krebbers authored Jul 05, 2019
  
  4a624063
- Add lemma `big_sepL2_reverse`. · d392b7a6
  Robbert Krebbers authored Jul 05, 2019
  
  d392b7a6
03 Jul, 2019 4 commits
- Merge branch 'ralf/update' into 'master' · 18d6dd40
  Ralf Jung authored Jul 03, 2019
```
provide a lemma to update only the authoritative part, ignoring the fragments entirely

See merge request !284
```
  18d6dd40
- Stronger local update for multisets that entails the old ones. · 649c6e79
  Robbert Krebbers authored Jul 03, 2019
  
  649c6e79
- Add lemmas for `≼` of `Cinl` and `Cinr`. · a18865f7
  Robbert Krebbers authored Jul 03, 2019
  
  a18865f7
- provide a lemma to update only the authoritative part, ignoring the fragments entirely · 22e1622c
  Ralf Jung authored Jul 03, 2019
  
  22e1622c
01 Jul, 2019 4 commits
- Merge branch 'ralf/eq' into 'master' · 6e79f000
  Ralf Jung authored Jul 01, 2019
```
heap_lang: Make binary "=" operator partial, to sync with CmpXchg

Closes #248

See merge request iris/iris!283
```
  6e79f000
- Make `iPure` non-local so it can be used for defining custom `iDestruct`-like tactics. · 1ee1d9f9
  Robbert Krebbers authored Jul 01, 2019
  
  1ee1d9f9
- use decide instead of bool_decide where possible · cb27aa7f
  Ralf Jung authored Jul 01, 2019
  
  cb27aa7f
- minor tweaks · 1889960b
  Ralf Jung authored Jul 01, 2019
  
  1889960b
30 Jun, 2019 2 commits
- bump std++ · 24ee24e2
  Ralf Jung authored Jun 30, 2019
  
  24ee24e2
- Bump stdpp. · 457a4b4e
  Robbert Krebbers authored Jun 30, 2019
  
  457a4b4e
29 Jun, 2019 1 commit

heap_lang: Make binary "=" operator partial, to sync with CmpXchg · 9e18501a

Ralf Jung authored Jun 28, 2019

This also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.

9e18501a

28 Jun, 2019 4 commits
- Bump std++. · 5b3f7de1
  Robbert Krebbers authored Jun 29, 2019
  
  5b3f7de1
- Up to 15 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 82bd1095
  Robbert Krebbers authored Jun 28, 2019
```
This commit made me cry...
```
  82bd1095
- Bump stdpp. · 61da8709
  Robbert Krebbers authored Jun 28, 2019
  
  61da8709
- Up to 14 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 8dc59df2
  Robbert Krebbers authored Jun 28, 2019
  
  8dc59df2
27 Jun, 2019 3 commits
- Bump stdpp. · 1b53e5dd
  Robbert Krebbers authored Jun 27, 2019
  
  1b53e5dd
- Up to 12 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`. · d5c0458f
  Robbert Krebbers authored Jun 27, 2019
```
Created this commit with pain in my heart!
```
  d5c0458f
- Merge branch 'ralf/auth-core-id' into 'master' · 57e5d1ed
  Robbert authored Jun 27, 2019
```
show auth_update_core_id

See merge request iris/iris!282
```
  57e5d1ed