Commits · master · Léo Stefanesco / examples

07 Aug, 2020 1 commit
- fix and test building with Coq 8.12 · a6257e34
  Ralf Jung authored Aug 07, 2020
  
  a6257e34
23 Jul, 2020 1 commit
- fix some warnings that show up with Coq 8.12 · 02de3e6c
  Ralf Jung authored Jul 23, 2020
  
  02de3e6c
22 Jul, 2020 1 commit
- Bump Iris (iIntros ?). · adf116ce
  Robbert Krebbers authored Jul 22, 2020
  
  adf116ce
21 Jul, 2020 1 commit
- Bump Iris (iExists ?). · ea96da9e
  Robbert Krebbers authored Jul 21, 2020
  
  ea96da9e
17 Jul, 2020 3 commits
- Merge branch 'cg-bag' into 'master' · f25d1b45
  Ralf Jung authored Jul 17, 2020
```
Add bag and tweak lock

See merge request iris/examples!36
```
  f25d1b45
- Minor tweaks to bag example · a9465820
  Simon Friis Vindum authored Jul 17, 2020
  
  a9465820
- Add bag and tweak lock · 80c70aff
  Simon Friis Vindum authored Jun 04, 2020
  
  80c70aff
16 Jul, 2020 1 commit
- update Makefile · ae60f103
  Ralf Jung authored Jul 16, 2020
  
  ae60f103
15 Jul, 2020 4 commits
- Bump Iris. · 504e128e
  Robbert Krebbers authored Jul 15, 2020
  
  504e128e
- update dependencies · 54c642e4
  Ralf Jung authored Jul 15, 2020
  
  54c642e4
- remove unused dec_agree import · 29bb2b2e
  Ralf Jung authored Jul 15, 2020
  
  29bb2b2e
- update dependencies · 92896ca3
  Ralf Jung authored Jul 15, 2020
  
  92896ca3
11 Jul, 2020 1 commit
- Merge branch 'clarify-which-bsd' into 'master' · 53c7fde4
  Ralf Jung authored Jul 11, 2020
```
LICENSE: Clarify which BSD license is being used

See merge request iris/examples!40
```
  53c7fde4
10 Jul, 2020 1 commit
- LICENSE: Clarify which BSD license is being used · d7a817e5
  Paolo G. Giarrusso authored Jul 10, 2020
```
Sister MR to iris!472.
```
  d7a817e5
08 Jul, 2020 1 commit
- adjust logatom terminology to match ReLoC 2 paper · 4de135d9
  Ralf Jung authored Jul 08, 2020
  
  4de135d9
30 Jun, 2020 5 commits
- README: make link texts consistent with folder names · 06827859
  Ralf Jung authored Jun 30, 2020
  
  06827859
- Merge branch 'array-lock' into 'master' · 77ea6399
  Ralf Jung authored Jun 30, 2020
```
Add array-based queuing lock example

See merge request iris/examples!34
```
  77ea6399
- Apply suggestion to Makefile.coq.local · 07c69b23
  Simon Friis Vindum authored Jun 30, 2020
  
  07c69b23
- Apply suggestion to Makefile.coq.local · bb75ce16
  Simon Friis Vindum authored Jun 30, 2020
  
  bb75ce16
- Fix makefile · 0580dbc5
  Simon Friis Vindum authored Jun 30, 2020
  
  0580dbc5
22 Jun, 2020 14 commits
- Use min_nat from Iris · 91723bb8
  Simon Friis Vindum authored Jun 22, 2020
  
  91723bb8
- Box add with bound RA · 17708f45
  Simon Friis Vindum authored Jun 17, 2020
  
  17708f45
- Construct RA out of min_nat RA · fc55272c
  Simon Friis Vindum authored Jun 17, 2020
  
  fc55272c
- Add ending newline to _CoqProject · de71ffe9
  Simon Friis Vindum authored Jun 11, 2020
  
  de71ffe9
- Shorten RA mixin proof · a1fb6a18
  Simon Friis Vindum authored Jun 11, 2020
  
  a1fb6a18
- Add comments, add entry in makefile · d5594f12
  Simon Friis Vindum authored Jun 04, 2020
  
  d5594f12
- Make changes based on feedback · b45c56d3
  Simon Friis Vindum authored Jun 01, 2020
  
  b45c56d3
- Better handling of numbers, refactor mod_fact proof · df35f4f0
  Simon Friis Vindum authored May 29, 2020
  
  df35f4f0
- Make changes in response to feedback · 8d303348
  Simon Friis Vindum authored May 29, 2020
  
  8d303348
- Refactor proof without `len` lemmas · 3b0fbbc2
  Simon Friis Vindum authored May 22, 2020
  
  3b0fbbc2
- Collect RAs in a single type class · a07771d0
  Simon Friis Vindum authored May 21, 2020
  
  a07771d0
- Make changes in response to feedback · b193e3b7
  Simon Friis Vindum authored May 20, 2020
  
  b193e3b7
- Refactor proofs and add comments · 32b6d46a
  Simon Friis Vindum authored May 18, 2020
  
  32b6d46a
- Add array-based queuing lock example · 5887e8da
  Simon Friis Vindum authored May 14, 2020
  
  5887e8da
19 Jun, 2020 4 commits
- iris-string-ident is not compatible with Coq 8.12 · a966fe18
  Ralf Jung authored Jun 19, 2020
  
  a966fe18
- nightly build against 8.12 beta · 2fc15ff2
  Ralf Jung authored Jun 19, 2020
  
  2fc15ff2
- bump Coq to 8.11.2, and also test Coq 8.12 beta · a8751afc
  Ralf Jung authored Jun 19, 2020
  
  a8751afc
- update Makefile · d2bd9890
  Ralf Jung authored Jun 19, 2020
  
  d2bd9890
18 Jun, 2020 2 commits
- Merge branch 'update-dependencies' into 'master' · a47a58c1
  Ralf Jung authored Jun 18, 2020
```
Update dependencies

See merge request iris/examples!39
```
  a47a58c1
- Update dependencies · ef5bf109
  Simon Friis Vindum authored Jun 18, 2020
  
  ef5bf109