Commits · 7788ff6f7d4550c8fc3c33f21690da85b4cb67bc · Lennard Gäher / Iris

17 Jun, 2020 1 commit
- adjust makefile for vos/vok and tutorials · 7788ff6f
  Ralf Jung authored Jun 17, 2020
  
  7788ff6f
15 Jun, 2020 2 commits

Merge branch 'fix-wp-pure' into 'master' · e84de6cc
Robbert Krebbers authored Jun 15, 2020
```
Use [fill K] in tac_wp_pure

See merge request iris/iris!463
```
e84de6cc

Tej Chajed authored Jun 15, 2020

This is more consistent with other tac_wp tactics for HeapLang and also
a tiny bit more efficient, which is good to embody in the basic tactics
so derived code follows the same patterns.

f9d6ada1

12 Jun, 2020 2 commits

Merge branch 'fix-specialize-error-message' into 'master' · 995dc37b
Robbert Krebbers authored Jun 12, 2020
```
Fix error message when with [% //] fails

Closes #325

See merge request iris/iris!460
```
995dc37b

Fix error message when with [% //] fails · 1aec27cb

Tej Chajed authored Jun 12, 2020

Fixes #325.

Also added a tests for the various `iSpecialize` error cases involving
the `[%]` and `[//]` specialization patterns.

1aec27cb

11 Jun, 2020 4 commits
- Merge branch 'robbert/loeb_weak' into 'master' · 11f9d567
  Ralf Jung authored Jun 11, 2020
```
Factor out lemma `löb_weak`.

See merge request iris/iris!459
```
  11f9d567
- Introduce notation `BiLaterContractive PROP` for `Contractive (bi_later (PROP:=PROP))`. · b57797ee
  Robbert Krebbers authored Jun 11, 2020
  
  b57797ee
- Use `löb_weak` for BiLöb class. · ee49d97b
  Robbert Krebbers authored Jun 11, 2020
  
  ee49d97b
- Factor out lemma `löb_weak`. · 725ffc11
  Robbert Krebbers authored Jun 08, 2020
  
  725ffc11
08 Jun, 2020 1 commit
- adjust \min font · ada31c02
  Ralf Jung authored Jun 08, 2020
  
  ada31c02
07 Jun, 2020 2 commits
- remove the weaker counterexample (now that the other one only requires a boring cinv_alloc) · 56e966fd
  Ralf Jung authored Jun 07, 2020
  
  56e966fd
- linear counterexample: we do not actually need cinv_alloc to be that powerful · 827f464c
  Ralf Jung authored Jun 07, 2020
  
  827f464c
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 Krebbers authored May 29, 2020
```
Change ascii turnstile

See merge request iris/iris!435
```
  c8bacab9
- change |-- to |- · 7b7d3336
  Gregory Malecha authored May 29, 2020 and Robbert Krebbers committed 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 Krebbers authored May 28, 2020
```
Fix `forall` parsing.

See merge request iris/iris!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 Krebbers authored May 28, 2020
```
Remove `Open Scope Z_scope` in HeapLang

See merge request iris/iris!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 iris/iris!457
```
  2643cb7d
- Merge branch 'plainly-scope' into 'master' · 0c21e4d7
  Robbert Krebbers authored May 28, 2020
```
Fix scopes for `plainly` following !456.

See merge request iris/iris!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 Krebbers authored May 28, 2020
```
Fix scopes of bupd and fupd

See merge request iris/iris!456
```
  288c5ea8
- Fix scopes of bupd and fupd · a3cc36e4
  Paolo G. Giarrusso authored May 28, 2020 and Robbert Krebbers committed 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 Krebbers authored May 27, 2020
```
Turn local instances ne_proper and ne_proper_2 into lemmas

See merge request iris/iris!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 1 commit
- Merge branch 'ralf/heap-lang-rename' into 'master' · d80e7abf
  Ralf Jung authored May 26, 2020
```
rename heap_lang modules

See merge request iris/iris!452
```
  d80e7abf