Commits · b7efc7bdc290bdc9efbde1bb040c7b65729e3341 · Lennard Gäher / Iris

25 May, 2020 1 commit
- rename array_tools -> array; update CHANGELOG · b7efc7bd
  Ralf Jung authored May 25, 2020
  
  b7efc7bd
22 May, 2020 1 commit
- clarify comment · 218d8b33
  Ralf Jung authored May 22, 2020
  
  218d8b33
20 May, 2020 4 commits
- test wp_free · 78116194
  Ralf Jung authored May 20, 2020
  
  78116194
- apply review suggestions · 84d2a9ea
  Ralf Jung authored May 20, 2020
  
  84d2a9ea
- test setoid_rewrite on inv_mapsto · fee2a24e
  Ralf Jung authored May 20, 2020
  
  fee2a24e
- make inv_mapsto for heap_lang proper definitions because they are higher-order · 83beac4e
  Ralf Jung authored May 20, 2020
  
  83beac4e
18 May, 2020 11 commits
- copy all gen_heap and gen_inv_heap mapsto lemmas, and name variables · 46b4463b
  Ralf Jung authored May 12, 2020
  
  46b4463b
- CHANGELOG, update gen_inv_heap comment · deb7703c
  Ralf Jung authored May 12, 2020
  
  deb7703c
- define and prove array_free · 3ec81a3d
  Ralf Jung authored May 12, 2020
  
  3ec81a3d
- add lifting lemma and tactic for single-location Free · 923d6b71
  Ralf Jung authored May 12, 2020
  
  923d6b71
- add single-location Free operation to language syntax and semantics · 16b2aefc
  Ralf Jung authored May 12, 2020
  
  16b2aefc
- note some design choices · 2c063fd4
  Ralf Jung authored May 07, 2020
  
  2c063fd4
- make heap store (option val) in preparation for deallocation · 522e0304
  Ralf Jung authored May 07, 2020
  
  522e0304
- document our breaking-changes-notification system · fdda97e8
  Ralf Jung authored May 18, 2020
  
  fdda97e8
- Merge branch 'ralf/inv_heap' into 'master' · 3d135daa
  Ralf Jung authored May 18, 2020
```
heap_lang lifting: instantiate inv_heapG and inv_heap_inv

See merge request iris/iris!429
```
  3d135daa
- changelog · 48787e36
  Ralf Jung authored May 18, 2020
  
  48787e36
- exhaustive match for lit_is_unboxed · 41400739
  Ralf Jung authored May 18, 2020
  
  41400739
16 May, 2020 2 commits
- Merge branch 'use-lia' into 'master' · 3a3f0706
  Ralf Jung authored May 16, 2020
```
Use lia to avoid omega deprecation warnings

Closes #319

See merge request iris/iris!445
```
  3a3f0706
- Use lia to avoid omega deprecation warnings · d7d078a9
  Tej Chajed authored May 16, 2020
```
Fixes #319
```
  d7d078a9
15 May, 2020 3 commits
- Merge branch 'robbert/twp_vals_compare_safe' into 'master' · 5cb8bc17
  Ralf Jung authored May 15, 2020
```
Also use `solve_vals_compare_safe` in TWP case of `wp_pure`.

See merge request iris/iris!444
```
  5cb8bc17
- Test cases. · 91cc6ffc
  Robbert Krebbers authored May 15, 2020
  
  91cc6ffc
- Also use `solve_vals_compare_safe` in TWP case of `wp_pure`. · 9917cdfa
  Robbert Krebbers authored May 15, 2020
  
  9917cdfa
14 May, 2020 2 commits
- update a reference to long-gone double_neation module · a5eb66d3
  Ralf Jung authored May 14, 2020
  
  a5eb66d3
- make inv_heapG part of heapG · bd9a61e5
  Ralf Jung authored May 14, 2020
  
  bd9a61e5
13 May, 2020 4 commits
- Merge branch 'big_sepL-inv' into 'master' · ffacaa03
  Robbert Krebbers authored May 13, 2020
```
Add big_sepL2_nil_inv_l/r.

See merge request iris/iris!442
```
  ffacaa03
- Add big_sepL2_nil_inv_l/r. · b31d8c00
  Dan Frumin authored May 13, 2020 and Robbert Krebbers committed May 13, 2020
  
  b31d8c00
- Merge branch 'ralf/lang-axioms' into 'master' · 976b02f6
  Ralf Jung authored May 13, 2020
```
Explain our language axioms better

Closes #271

See merge request iris/iris!440
```
  976b02f6
- update dependencies · 635cdf1e
  Ralf Jung authored May 13, 2020
  
  635cdf1e
12 May, 2020 2 commits
- rename lemma variable names for more clarity · 7a4f28b1
  Ralf Jung authored May 12, 2020
  
  7a4f28b1
- tweak wording · 6019fde6
  Ralf Jung authored May 12, 2020
  
  6019fde6
11 May, 2020 4 commits
- Add lemma `exist_wand_forall`, similar to `exist_impl_forall`. · c6bcaade
  Robbert Krebbers authored May 11, 2020
  
  c6bcaade
- tweak proof · 0b467975
  Ralf Jung authored May 11, 2020
  
  0b467975
- tweak comments · 19e984a6
  Ralf Jung authored May 11, 2020
  
  19e984a6
- explain our langauge axioms better · cd8b29fe
  Ralf Jung authored May 11, 2020
  
  cd8b29fe
08 May, 2020 1 commit
- Merge branch 'ralf/select' into 'master' · bc45284f
  Ralf Jung authored May 08, 2020
```
use new select tactic from std++

See merge request iris/iris!438
```
  bc45284f
07 May, 2020 3 commits
- update dependencies · 701b533c
  Ralf Jung authored May 07, 2020
  
  701b533c
- use new select tactic from std++ · 111c0332
  Ralf Jung authored May 07, 2020
  
  111c0332
- update dependencies · 858665ff
  Ralf Jung authored May 07, 2020
  
  858665ff
05 May, 2020 1 commit
- build-all: test slow projects first and fast ones later · 870a4f78
  Ralf Jung authored May 05, 2020
  
  870a4f78
01 May, 2020 1 commit
- Merge branch 'core-id-local-update' into 'master' · b4a6bd33
  Ralf Jung authored May 01, 2020
```
Make core_id_local_update work with fractional authority

See merge request iris/iris!430
```
  b4a6bd33