Commits · 94533e337053c12968e6f25a800066ebe248688d · Yixuan Chen / Iris

Jul 13, 2019
- proper link and less Rust ;) · 94533e33
  Ralf Jung authored 5 years ago
  
  94533e33
- erasure is in iris/examples · b5e2eb4e
  Ralf Jung authored 5 years ago
  
  b5e2eb4e
- Weaken premise of `gmultiset_local_update_dealloc`. · 736b17dc
  Robbert Krebbers authored 5 years ago
  
  736b17dc
- Merge branch 'ralf/pair-core' into 'master' · 8f41613d
  Robbert Krebbers authored 5 years ago
  
  show that pair construction commutes with taking the core See merge request iris/iris!286
  8f41613d
- shorten proof · 162755de
  Ralf Jung authored 5 years ago
  
  162755de
Jul 12, 2019
- tweak proof to also work after a Coq bugfix · e6f6758c
  Ralf Jung authored 5 years ago
  
  e6f6758c
- changelog for comparison changes · f455b5d4
  Ralf Jung authored 5 years ago
  
  f455b5d4
Jul 09, 2019
- dont quantify over empty telescopes · c2eaa77d
  Ralf Jung authored 5 years ago
  
  c2eaa77d
- Merge branch 'fresh_locs_arg' into 'master' · 64c16f99
  Robbert Krebbers authored 5 years ago
  
  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 5 years ago
  
  80623a8c
- bump std++ · 5123ac6b
  Ralf Jung authored 5 years ago
  
  5123ac6b
Jul 07, 2019
- show that pair cosntruction commutes with taking the core · c2d34fe3
  Ralf Jung authored 5 years ago
  
  c2d34fe3
Jul 05, 2019
- Bump stdpp. · 4a624063
  Robbert Krebbers authored 5 years ago
  
  4a624063
- Add lemma `big_sepL2_reverse`. · d392b7a6
  Robbert Krebbers authored 5 years ago
  
  d392b7a6
Jul 03, 2019
- Merge branch 'ralf/update' into 'master' · 18d6dd40
  Ralf Jung authored 5 years ago
  
  provide a lemma to update only the authoritative part, ignoring the fragments entirely See merge request iris/iris!284
  18d6dd40
- Stronger local update for multisets that entails the old ones. · 649c6e79
  Robbert Krebbers authored 5 years ago
  
  649c6e79
- Add lemmas for `≼` of `Cinl` and `Cinr`. · a18865f7
  Robbert Krebbers authored 5 years ago
  
  a18865f7
- provide a lemma to update only the authoritative part, ignoring the fragments entirely · 22e1622c
  Ralf Jung authored 5 years ago
  
  22e1622c
Jul 01, 2019
- Merge branch 'ralf/eq' into 'master' · 6e79f000
  Ralf Jung authored 5 years ago
  
  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 5 years ago
  
  1ee1d9f9
- use decide instead of bool_decide where possible · cb27aa7f
  Ralf Jung authored 5 years ago
  
  cb27aa7f
- minor tweaks · 1889960b
  Ralf Jung authored 5 years ago
  
  1889960b
Jun 30, 2019
- bump std++ · 24ee24e2
  Ralf Jung authored 5 years ago
  
  24ee24e2
- Bump stdpp. · 457a4b4e
  Robbert Krebbers authored 5 years ago
  
  457a4b4e
Jun 29, 2019

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

Ralf Jung authored 5 years ago

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

9e18501a

Jun 28, 2019
- Bump std++. · 5b3f7de1
  Robbert Krebbers authored 5 years ago
  
  5b3f7de1
- Up to 15 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 82bd1095
  Robbert Krebbers authored 5 years ago
  
  This commit made me cry...
  82bd1095
- Bump stdpp. · 61da8709
  Robbert Krebbers authored 5 years ago
  
  61da8709
- Up to 14 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 8dc59df2
  Robbert Krebbers authored 5 years ago
  
  8dc59df2
Jun 27, 2019
- Bump stdpp. · 1b53e5dd
  Robbert Krebbers authored 5 years ago
  
  1b53e5dd
- Up to 12 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`. · d5c0458f
  Robbert Krebbers authored 5 years ago
  
  Created this commit with pain in my heart!
  d5c0458f
- Merge branch 'ralf/auth-core-id' into 'master' · 57e5d1ed
  Robbert Krebbers authored 5 years ago
  
  show auth_update_core_id See merge request iris/iris!282
  57e5d1ed
- show auth_update_core_id · 1a15694e
  Ralf Jung authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  1a15694e
Jun 26, 2019
- bump std++ · 4832f461
  Ralf Jung authored 5 years ago
  
  4832f461
- Bump stdpp. · ad3e5066
  Robbert Krebbers authored 5 years ago
  
  ad3e5066
Jun 25, 2019
- Merge branch 'sigT_equivI-admissible' into 'master' · 6a86d925
  Robbert Krebbers authored 5 years ago
  
  Prove sigT_equivI is admissible (fix #250) Closes #250 See merge request iris/iris!280
  6a86d925
- Prove sigT_equivI is admissible (fix #250) · 25c5e64d
  Paolo G. Giarrusso authored 5 years ago
  
  Verified
  
  25c5e64d
- Prove `existT a` is NonExpansive & Proper · ffc56091
  Paolo G. Giarrusso authored 5 years ago
  
  One of the new proofs needs `sigTO`, so move others together.
  Verified
  
  ffc56091
- Fix another typo. · 1ec2a309
  Robbert Krebbers authored 5 years ago
  
  1ec2a309
Jun 24, 2019
- Merge branch 'pg/typo-fix' into 'master' · 1ad44fff
  Ralf Jung authored 5 years ago
  
  Fix typos in comments See merge request iris/iris!281
  1ad44fff