Commits · 4c7f8414966b723956b03eaf6f2da75a6a34d1c8 · Marianna Rapoport / iris-coq

13 Dec, 2017 3 commits
- superscript looks better · 4c7f8414
  Ralf Jung authored Dec 13, 2017
  
  4c7f8414
- consistently use new stateinterp notation · e2a144ed
  Ralf Jung authored Dec 13, 2017
  
  e2a144ed
- WP def.n tweaking · 7e2d2dbc
  Ralf Jung authored Dec 13, 2017
  
  7e2d2dbc
12 Dec, 2017 2 commits
- better section title · c2f75971
  Ralf Jung authored Dec 12, 2017
  
  c2f75971
- docs: WP stuckness · 9647cb87
  Ralf Jung authored Dec 12, 2017
  
  9647cb87
11 Dec, 2017 8 commits
- typo · a1fbc5c9
  Ralf Jung authored Dec 11, 2017
  
  a1fbc5c9
- docs: typo · c3585db7
  Ralf Jung authored Dec 11, 2017
  
  c3585db7
- move the dynamic composeable higher-order ghost state logic up so it does not... · c83e64a1
  Ralf Jung authored Dec 11, 2017
```
move the dynamic composeable higher-order ghost state logic up so it does not seem to depend on  a language
```
  c83e64a1
- cancellable invariants · d48b2c6a
  Ralf Jung authored Dec 11, 2017
  
  d48b2c6a
- describe frac RA · 82aa84a7
  Ralf Jung authored Dec 11, 2017
  
  82aa84a7
- refer to journal paper · a007ecf5
  Ralf Jung authored Dec 11, 2017
  
  a007ecf5
- more experimental changelog · 042393e6
  Ralf Jung authored Dec 11, 2017
  
  042393e6
- changelog · df0f72f0
  Ralf Jung authored Dec 11, 2017
  
  df0f72f0
10 Dec, 2017 22 commits
- fix title from assertion -> proposition rename · 30f50796
  Ralf Jung authored Dec 10, 2017
  
  30f50796
- Docs: Do not abbreviate. · b6fb28b7
  Robbert Krebbers authored Dec 10, 2017
  
  b6fb28b7
- Docs: assertion → proposition (as in the ground up paper). · bf46989d
  Robbert Krebbers authored Dec 10, 2017
  
  bf46989d
- Docs: remark about name "Camera". · e1f4aaad
  Robbert Krebbers authored Dec 10, 2017
  
  e1f4aaad
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq · 46313843
  Ralf Jung authored Dec 10, 2017
  
  46313843
- fix a caption · 05f201af
  Ralf Jung authored Dec 10, 2017
  
  05f201af
- Docs: CMRA → Camera (as in the Ground Up paper). · 03fe24e2
  Robbert Krebbers authored Dec 10, 2017
  
  03fe24e2
- missed a caption · fd729747
  Ralf Jung authored Dec 10, 2017
  
  fd729747
- fix captialization · d31256c0
  Ralf Jung authored Dec 10, 2017
  
  d31256c0
- Revert "Docs: fix capitals of section." · d96f252e
  Ralf Jung authored Dec 10, 2017
```
This reverts commit 7a6d36c6.
```
  d96f252e
- Docs: fix capitals of section. · 7a6d36c6
  Robbert Krebbers authored Dec 10, 2017
  
  7a6d36c6
- Docs: fix typo. · b2e7e52f
  Robbert Krebbers authored Dec 10, 2017
  
  b2e7e52f
- 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 5 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