Commits · b9c5f9b654e5cd0b02d5c14dbda505f6c4fdca8a · Marianna Rapoport / iris-coq

10 Dec, 2017 10 commits
- Docs: use \stateinterp macro. · b9c5f9b6
  Robbert Krebbers authored Dec 10, 2017
  
  b9c5f9b6
- Docs: use \venv macro. · 604ad636
  Robbert Krebbers authored Dec 10, 2017
  
  604ad636
- Docs: update iris.sty. · 49bb4194
  Robbert Krebbers authored Dec 10, 2017
```
Merge it with the JFP paper, we probably need to backport it there.
```
  49bb4194
- docs: banach: make f^k part of the theorem, nut just a remark; extend ref to america-rutten · 40474920
  Ralf Jung authored Dec 10, 2017
  
  40474920
- Docs: fix reference to America/Rutten. · 8a2a27eb
  Robbert Krebbers authored Dec 10, 2017
  
  8a2a27eb
- Docs: fix references to Banach. · 4912a660
  Robbert Krebbers authored Dec 10, 2017
  
  4912a660
- Bump std++. · 8d1b4d4c
  Robbert Krebbers authored Dec 10, 2017
  
  8d1b4d4c
- Docs: put Banach and America/Rutten in a theorem environment. · 861ee760
  Robbert Krebbers authored Dec 10, 2017
  
  861ee760
- Fix typo in docs: fixpoints can only be taken of endo-functions. · c73f0c68
  Robbert Krebbers authored Dec 10, 2017
  
  c73f0c68
- fix a LeTeX warning · 4cb0d91d
  Ralf Jung authored Dec 10, 2017
  
  4cb0d91d
08 Dec, 2017 6 commits
- Merge branch 'jh/upred_alt' into 'master' · 3f321758
  Jacques-Henri Jourdan authored Dec 08, 2017
```
Prove that uPred is complete even if we remove the validity restriction in uPred_closed.

See merge request FP/iris-coq!99
```
  3f321758
- fix typos; add comment · a603fe3a
  Ralf Jung authored Dec 08, 2017
  
  a603fe3a
- on unique representatives · d4aa9dd9
  Ralf Jung authored Dec 08, 2017
  
  d4aa9dd9
- uPred: show that the definition in the appendix is equivalent to the one in Coq · 1df177bd
  Ralf Jung authored Dec 08, 2017
  
  1df177bd
- move comment up · a27982f7
  Ralf Jung authored Dec 08, 2017
  
  a27982f7
- update docs: new upred definition, sProp for validity · af017171
  Ralf Jung authored Dec 08, 2017
  
  af017171
07 Dec, 2017 10 commits
- fix a lemma that did not use its stuckness · bba89517
  Ralf Jung authored Dec 07, 2017
  
  bba89517
- make strongly_atomic_atomic more convenient · 94922d09
  Ralf Jung authored Dec 07, 2017
  
  94922d09
- fix build after merging · e76ca2de
  Ralf Jung authored Dec 07, 2017
  
  e76ca2de
- rename adequate_safe -> adequate_not_stuck · c5fa01fe
  Ralf Jung authored Dec 07, 2017
  
  c5fa01fe
- Merge branch 'swasey/progress2' into 'master' · f8890ff9
  Ralf Jung authored Dec 07, 2017
```
Add stuckness bits to WP.

See merge request FP/iris-coq!80
```
  f8890ff9
- CamlCase of inductive constructors · 0841a63d
  Ralf Jung authored Dec 07, 2017
  
  0841a63d
- Fix comment. · 908ea111
  Jacques-Henri Jourdan authored Dec 07, 2017
  
  908ea111
- Merge uPred_mono and uPred_closed. · e14e9ec2
  Jacques-Henri Jourdan authored Dec 07, 2017
  
  e14e9ec2
- remove unnecessary side-conditions from ownP lemmas · 52f90871
  Ralf Jung authored Dec 07, 2017
  
  52f90871
- Remove useless comment. · cbb493e7
  Jacques-Henri Jourdan authored Dec 07, 2017
  
  cbb493e7
06 Dec, 2017 4 commits
- Merge branch 'robbert/heap_lang_binop' into 'master' · a7b0f138
  Robbert Krebbers authored Dec 06, 2017
```
Add all the usual binary operators to heap_lang.

See merge request FP/iris-coq!97
```
  a7b0f138
- Typo. · 7678b4f9
  Jacques-Henri Jourdan authored Dec 06, 2017
  
  7678b4f9
- Remove upred_iso.v · e5dce071
  Jacques-Henri Jourdan authored Dec 06, 2017
  
  e5dce071
- Prove that uPred is complete even if we remove the validity · 9f8d9a5e
  Jacques-Henri Jourdan authored Dec 06, 2017
```
restriction in uPred_closed.
```
  9f8d9a5e
05 Dec, 2017 10 commits
- Add bitwise negation on integers. · 700646bc
  Robbert Krebbers authored Dec 05, 2017
  
  700646bc
- Update Changelog. · c57f36f0
  Robbert Krebbers authored Dec 05, 2017
  
  c57f36f0
- Add notations for some of the new heap_lang binary operators. · 17b5bd9a
  Robbert Krebbers authored Dec 05, 2017
  
  17b5bd9a
- Add all the usual binary operators to heap_lang. · 4782352f
  Robbert Krebbers authored Dec 05, 2017
  
  4782352f
- Merge branch 'robbert/faa' into 'master' · 450aef18
  Robbert Krebbers authored Dec 05, 2017
```
Add atomic fetch-and-add operation to heap_lang

Closes #120

See merge request FP/iris-coq!96
```
  450aef18
- Add Changelog entry. · 1c2ea26d
  Robbert Krebbers authored Dec 05, 2017
  
  1c2ea26d
- Test case for fetch-and-add. · 85245d48
  Robbert Krebbers authored Dec 04, 2017
  
  85245d48
- Add atomic fetch-and-add operation to heap_lang. · adb5b54a
  Robbert Krebbers authored Dec 04, 2017
  
  adb5b54a
- fix build · bb37a795
  Ralf Jung authored Dec 05, 2017
  
  bb37a795
- bump std++; use \sqsubseteq for stuckness_le · d819164f
  Ralf Jung authored Dec 05, 2017
  
  d819164f