Commits · ralf/wp_apply-no-simpl · Lennard Gäher / Iris

11 Nov, 2020 3 commits
- make wp_apply not call wp_pures · efbc0fdb
  Ralf Jung authored Nov 11, 2020
  
  efbc0fdb
- Merge branch 'ralf/notypeclasses' into 'master' · 1346311d
  Robbert Krebbers authored Nov 11, 2020
```
avoid (e)apply in wp_expr_eval

See merge request iris/iris!582
```
  1346311d
- avoid (e)apply in wp_expr_eval · 3e8220fc
  Ralf Jung authored Nov 11, 2020
  
  3e8220fc
10 Nov, 2020 28 commits
- Merge branch 'ralf/mapsto_ne' into 'master' · 832a63d6
  Ralf Jung authored Nov 10, 2020
```
Rename mapsto_mapsto_ne and add easier-to-use variant

See merge request !574
```
  832a63d6
- Add variant of mapsto_mapsto_ne that does not require further fraction reasoning · 07b3a7db
  Ralf Jung authored Nov 05, 2020
  
  07b3a7db
- fix build on older Coq · af752fbe
  Ralf Jung authored Nov 10, 2020
  
  af752fbe
- Merge branch 'ralf/gen-heap-init' into 'master' · 59c4621d
  Ralf Jung authored Nov 10, 2020
```
provide _big variant of gen_heap_init

Closes #361

See merge request !580
```
  59c4621d
- fix build · 36e790f8
  Ralf Jung authored Nov 10, 2020
  
  36e790f8
- one gen_heap_init lemma is enough · 79cd8d45
  Ralf Jung authored Nov 10, 2020
  
  79cd8d45
- Merge branch 'ralf/doc-equalities' into 'master' · 360fb4b6
  Ralf Jung authored Nov 10, 2020
```
Documentation on Iris equalities (take 2)

See merge request !575
```
  360fb4b6
- address feedback · 8695972d
  Ralf Jung authored Nov 10, 2020
  
  8695972d
- Apply 2 suggestion(s) to 1 file(s) · c568ece0
  Ralf Jung authored Nov 10, 2020
  
  c568ece0
- prefer _L · 3cb0702d
  Ralf Jung authored Nov 10, 2020
  
  3cb0702d
- provide _big variant of gen_heap_init · 8008c189
  Ralf Jung authored Nov 10, 2020
  
  8008c189
- rename gen_heap_alloc_gen -> gen_heap_alloc_big · 5e47e4ce
  Ralf Jung authored Nov 10, 2020
  
  5e47e4ce
- Merge branch 'ralf/ra-docs' into 'master' · 7d2bf3fa
  Ralf Jung authored Nov 10, 2020
```
split RA docs into separate file, and general doc updates

See merge request !576
```
  7d2bf3fa
- remove outdated 'm' metavaraibe; enable coq syntax highlighting · 3cd45dbc
  Ralf Jung authored Nov 10, 2020
  
  3cd45dbc
- Merge branch 'ralf/seal' into 'master' · 370aaa62
  Ralf Jung authored Nov 10, 2020
```
Seal ghost_var and mnat_own

See merge request iris/iris!571
```
  370aaa62
- seal mnat_own · 532954f2
  Ralf Jung authored Nov 05, 2020
  
  532954f2
- Merge branch 'ralf/wp-bind-empty' into 'master' · 98116d6a
  Ralf Jung authored Nov 10, 2020
```
fix wp_bind with empty context

See merge request iris/iris!579
```
  98116d6a
- changelog, TWP test · 672f4a53
  Ralf Jung authored Nov 10, 2020
  
  672f4a53
- fix typo in wp_value_head · 51057db0
  Ralf Jung authored Nov 09, 2020
  
  51057db0
- fix wp_bind with empty context · 7791266a
  Ralf Jung authored Nov 09, 2020
  
  7791266a
- Merge branch 'ralf/wp-pures-val' into 'master' · 3bd32904
  Ralf Jung authored Nov 10, 2020
```
wp_pures: also handle [WP v]

See merge request iris/iris!578
```
  3bd32904
- also test TWP · 74d678e2
  Ralf Jung authored Nov 10, 2020
  
  74d678e2
- Fix compilation with Coq 8.10 (lia is weaker). · 8fab551a
  Robbert Krebbers authored Nov 10, 2020
  
  8fab551a
- Merge branch 'ralf/gmap-view-valid' into 'master' · 834105d1
  Ralf Jung authored Nov 10, 2020
```
gmap_view: add some missing validity lemmas

See merge request iris/iris!573
```
  834105d1
- Merge branch 'array_init' into 'master' · 574bd5e8
  Ralf Jung authored Nov 10, 2020
```
Add `array_init` and corresponding WP specs.

See merge request iris/iris!492
```
  574bd5e8
- Make indentation consistent. · fc43b4fa
  Robbert Krebbers authored Nov 10, 2020
  
  fc43b4fa
- fix import ordering · c48296a0
  Ralf Jung authored Nov 10, 2020
  
  c48296a0
- add docs and changelog entry · 0e228686
  Ralf Jung authored Nov 10, 2020
  
  0e228686
09 Nov, 2020 1 commit
- wp_pures: also handle [WP v] · 57a3c4ff
  Ralf Jung authored Nov 09, 2020
  
  57a3c4ff
06 Nov, 2020 6 commits
- Merge branch 'finish-strict-bulleting' into 'master' · 2bcaf8ba
  Ralf Jung authored Nov 06, 2020
```
Enforce strict bulleting

Closes #344

See merge request iris/iris!577
```
  2bcaf8ba
- Enforce strict bulleting · 73ea819d
  Tej Chajed authored Nov 06, 2020
```
Finishes the work started in !563.

Fixes #344
```
  73ea819d
- Merge branch 'strict-bulleting' into 'master' · ad7fd9c0
  Ralf Jung authored Nov 06, 2020
```
Make bulleting strict for algebra and base_logic

See merge request iris/iris!563
```
  ad7fd9c0
- editing of equalities documentation · b85bebc3
  Ralf Jung authored Nov 06, 2020
  
  b85bebc3
- split RA docs into separate file, and general doc updates · 8cfe4ceb
  Ralf Jung authored Nov 06, 2020
  
  8cfe4ceb
- Documentation on Iris equalities · d8e8dfea
  Paolo G. Giarrusso authored Aug 09, 2019 and Ralf Jung committed Nov 06, 2020
  
  d8e8dfea
05 Nov, 2020 2 commits
- Merge branch 'intuitionistic_sep_dup' into 'master' · 56b76032
  Ralf Jung authored Nov 05, 2020
```
Strengthen persistent_sep_dup for intuitionistic propositions

See merge request iris/iris!556
```
  56b76032
- Strengthen persistent_sep_dup for intuitionistic propositions · 13c5c1ad
  Paolo G. Giarrusso authored Nov 05, 2020 and Ralf Jung committed Nov 05, 2020
  
  13c5c1ad