Commits · master · Iris / Iris

06 Jun, 2020 2 commits
- capitalize Emp consistent with True/False · d1982040
  Ralf Jung authored Jun 07, 2020
  
  d1982040
- make local update font consistent with other notation · a7b651f5
  Ralf Jung authored Jun 06, 2020
  
  a7b651f5
04 Jun, 2020 1 commit
- avoid ugly page break after judgment header · 0000e975
  Ralf Jung authored Jun 04, 2020
  
  0000e975
03 Jun, 2020 1 commit
- add TeX Makefile · 7fb5dd20
  Ralf Jung authored Jun 03, 2020
  
  7fb5dd20
01 Jun, 2020 1 commit
- tweak spacing around our domains · b880d5a2
  Ralf Jung authored Jun 01, 2020
  
  b880d5a2
30 May, 2020 1 commit
- sync iris.sty with my thesis, and small tweaks · 1c4f0990
  Ralf Jung authored May 30, 2020
  
  1c4f0990
29 May, 2020 6 commits
- Merge branch 'change-turnstile' into 'master' · c8bacab9
  Robbert authored May 29, 2020
```
Change ascii turnstile

See merge request !435
```
  c8bacab9
- change |-- to |- · 7b7d3336
  Gregory Malecha authored May 29, 2020
```
- it doesn't seem to conflict with anything in Ltac
```
  7b7d3336
- Coq 8.11.2 tag exists but there is no such release · e4fad281
  Ralf Jung authored May 29, 2020
  
  e4fad281
- test Coq 8.11.2, and the Coq 8.12 branch · b9c2ad9d
  Ralf Jung authored May 29, 2020
  
  b9c2ad9d
- update dependencies · bd4f4625
  Ralf Jung authored May 29, 2020
  
  bd4f4625
- fix proofmode_ascii test on latest Coq · 2f5ef3ed
  Ralf Jung authored May 29, 2020
  
  2f5ef3ed
28 May, 2020 11 commits
- Merge branch 'fix-forall-parsing' into 'master' · 9830590f
  Robbert authored May 28, 2020
```
Fix `forall` parsing.

See merge request !432
```
  9830590f
- Fix `forall` parsing. using the stdpp change · 6ada4936
  Gregory Malecha authored Apr 22, 2020
  
  6ada4936
- Merge branch 'robbert/open_scope_Z' into 'master' · 38f177d3
  Robbert authored May 28, 2020
```
Remove `Open Scope Z_scope` in HeapLang

See merge request !453
```
  38f177d3
- CHANGELOG entry. · 9d99d63c
  Robbert Krebbers authored May 28, 2020
  
  9d99d63c
- Remove `Open Scope Z_scope` in HeapLang. · 9d820c00
  Robbert Krebbers authored May 27, 2020
  
  9d820c00
- Merge branch 'ci/robbert/I' into 'master' · 2643cb7d
  Ralf Jung authored May 28, 2020
```
Remove redundant `%I` scopes in definitions.

See merge request !457
```
  2643cb7d
- Merge branch 'plainly-scope' into 'master' · 0c21e4d7
  Robbert authored May 28, 2020
```
Fix scopes for `plainly` following !456.

See merge request !458
```
  0c21e4d7
- Fix scopes for `plainly` following !456 . · 7458fa67
  Paolo G. Giarrusso authored May 28, 2020
  
  7458fa67
- Remove redundant `%I` scopes in definitions. · 5dff121a
  Robbert Krebbers authored May 28, 2020
  
  5dff121a
- Merge branch 'bfupd-scopes' into 'master' · 288c5ea8
  Robbert authored May 28, 2020
```
Fix scopes of bupd and fupd

See merge request !456
```
  288c5ea8
- Fix scopes of bupd and fupd · a3cc36e4
  Paolo G. Giarrusso authored May 28, 2020
  
  a3cc36e4
27 May, 2020 4 commits
- update dependencies · e2c87974
  Ralf Jung authored May 28, 2020
  
  e2c87974
- update dependencies · 51c4156f
  Ralf Jung authored May 27, 2020
  
  51c4156f
- Merge branch 'lemma-not-instance' into 'master' · f050d84a
  Robbert authored May 27, 2020
```
Turn local instances ne_proper and ne_proper_2 into lemmas

See merge request !454
```
  f050d84a
- Turn local instances ne_proper and ne_proper_2 into lemmas · 329b8c2c
  Paolo G. Giarrusso authored May 27, 2020
  
  329b8c2c
26 May, 2020 2 commits
- Merge branch 'ralf/heap-lang-rename' into 'master' · d80e7abf
  Ralf Jung authored May 26, 2020
```
rename heap_lang modules

See merge request !452
```
  d80e7abf
- fix ex_mapsto fractional handling · e3f87a95
  Ralf Jung authored May 26, 2020
  
  e3f87a95
25 May, 2020 11 commits
- review feedback · 01d2e142
  Ralf Jung authored May 25, 2020
  
  01d2e142
- changelog · 97b9de6c
  Ralf Jung authored May 25, 2020
  
  97b9de6c
- rename heap_lang modules · 5d754755
  Ralf Jung authored May 25, 2020
  
  5d754755
- Merge branch 'robbert/loeb' into 'master' · 7186900b
  Robbert authored May 25, 2020
```
Prove different versions of Löb rule

See merge request !451
```
  7186900b
- Merge branch 'robbert/inv_combine' into 'master' · a5ffb5e8
  Ralf Jung authored May 25, 2020
```
Add lemma `inv_combine`.

See merge request !431
```
  a5ffb5e8
- CHANGELOG entry. · a74ff3bf
  Robbert Krebbers authored May 24, 2020
  
  a74ff3bf
- Add lemma `inv_combine_dup_l`. · 1dc2aecd
  Robbert Krebbers authored May 24, 2020
```
Thanks to @tchajed for the initial version of this proof.
```
  1dc2aecd
- Add lemma `inv_combine`. · ea29f3a0
  Robbert Krebbers authored Apr 21, 2020
  
  ea29f3a0
- Rename `inv_sep` into `env_split`. · 725d4329
  Robbert Krebbers authored May 24, 2020
  
  725d4329
- Merge branch 'ci/ralf/dealloc' into 'master' · e49f76e7
  Ralf Jung authored May 25, 2020
```
heap_lang: support deallocation

Closes #313

See merge request !439
```
  e49f76e7
- Simplify proof of `tac_löb` using new lemma `löb_wand_intuitionistically`. · 016cd820
  Robbert Krebbers authored May 25, 2020
  
  016cd820