Commits · master · Iris / examples

13 Jan, 2020 2 commits
- upgrade to opam 2 · 92275f5b
  Ralf Jung authored Jan 13, 2020
  
  92275f5b
- Small consistency fixes logrel heaplang. · b73553f9
  Robbert Krebbers authored Jan 13, 2020
  
  b73553f9
13 Dec, 2019 6 commits
- now this should work on 8.10 as well... sigh · e5b6840b
  Ralf Jung authored Dec 13, 2019
  
  e5b6840b
- Mostly revert the previous commit · ace0db94
  Ralf Jung authored Dec 13, 2019
```
It leads to wild unification errors on 8.11.  None of this makes any sense, but I guess that is expected with Coq...
```
  ace0db94
- fix more imports to hopefully work both on 8.10 and 8.11 · 5726c91c
  Ralf Jung authored Dec 13, 2019
  
  5726c91c
- fix the rest of the repo for Coq 8.11 · 89196687
  Ralf Jung authored Dec 13, 2019
  
  89196687
- make logatom work with Coq 8.11 · ea928791
  Ralf Jung authored Dec 13, 2019
  
  ea928791
- nightly test for 8.11 branch · 5fa6ed80
  Ralf Jung authored Dec 13, 2019
  
  5fa6ed80
21 Nov, 2019 2 commits
- remove prophecy erasure proof (it is in the main Iris repo now) · b19a5b84
  Ralf Jung authored Nov 21, 2019
  
  b19a5b84
- Bump Iris (`iPoseProof` changes). · de6dd885
  Robbert Krebbers authored Nov 21, 2019
  
  de6dd885
14 Nov, 2019 2 commits
- Merge branch 'rdcss_meta_token' into 'master' · a20140b8
  Ralf Jung authored Nov 14, 2019
```
Modification of the RDCSS example to use meta tokens

See merge request iris/examples!30
```
  a20140b8
- Modification of the RDCSS example to use meta tokens · bbf33b66
  Rodolphe Lepigre authored Nov 14, 2019
```
(and some cleanup)
```
  bbf33b66
13 Nov, 2019 3 commits
- fix comment · d731cb31
  Ralf Jung authored Nov 13, 2019
  
  d731cb31
- Merge branch 'rdcss_comment' into 'master' · 815b0180
  Ralf Jung authored Nov 13, 2019
```
Comment in the RDCSS spec about GClocs.

See merge request iris/examples!29
```
  815b0180
- Expand RDCSS comments · 6639940c
  Rodolphe Lepigre authored Nov 13, 2019
  
  6639940c
12 Nov, 2019 3 commits
- Merge branch 'typed_proph' into 'master' · 8de152b1
  Ralf Jung authored Nov 12, 2019
```
Typed prophecy variables + cleanup

See merge request iris/examples!28
```
  8de152b1
- Typed prophecy variables + cleanup · 0c551f14
  Rodolphe Lepigre authored Nov 12, 2019
  
  0c551f14
- Bump iris (no changes needed) · f2637250
  Ralf Jung authored Nov 12, 2019
  
  f2637250
07 Nov, 2019 8 commits
- Bump Iris. · 3092552d
  Robbert Krebbers authored Nov 07, 2019
  
  3092552d
- Merge branch 'ci/amin/fix-logrell-soundness' into 'master' · dd32b1ff
  Ralf Jung authored Nov 07, 2019
```
Fix logrel soundness proofs

See merge request iris/examples!27
```
  dd32b1ff
- Fix logrel soundness proofs · b95a80e0
  Amin Timany authored Nov 07, 2019
  
  b95a80e0
- link to opam repo commits for version numbers · a83f57e6
  Ralf Jung authored Nov 07, 2019
  
  a83f57e6
- rely on the new ocaml default · 53fab07f
  Ralf Jung authored Nov 07, 2019
  
  53fab07f
- fix ocaml version · f2c53bf9
  Ralf Jung authored Nov 07, 2019
  
  f2c53bf9
- switch CI to Coq 8.10.1 · f8f664fe
  Ralf Jung authored Nov 07, 2019
  
  f8f664fe
- update Makefile · 9612d208
  Ralf Jung authored Nov 07, 2019
  
  9612d208
06 Nov, 2019 1 commit
- and another 8.10 warning · 87ff31e9
  Ralf Jung authored Nov 06, 2019
  
  87ff31e9
02 Nov, 2019 2 commits
- bump Iris for LitErased -> LitPoison rename · 0c1aa0a0
  Ralf Jung authored Nov 02, 2019
  
  0c1aa0a0
- warnings management · 034e63b6
  Ralf Jung authored Nov 02, 2019
  
  034e63b6
31 Oct, 2019 1 commit
- Bump iris (no changes needed) · 57c481a9
  Ralf Jung authored Oct 31, 2019
  
  57c481a9
22 Oct, 2019 1 commit
- add some prophecy libs · 19c4dba6
  Ralf Jung authored Oct 22, 2019
  
  19c4dba6
19 Sep, 2019 1 commit
- Bump Iris. · 1813cb14
  Robbert Krebbers authored Sep 19, 2019
  
  1813cb14
29 Aug, 2019 2 commits
- credit where credit is due · 9795c36e
  Ralf Jung authored Aug 29, 2019
  
  9795c36e
- bump Iris · c0a33a82
  Ralf Jung authored Aug 29, 2019
  
  c0a33a82
14 Aug, 2019 1 commit
- more lemmas moved · 918aa45d
  Ralf Jung authored Aug 14, 2019
  
  918aa45d
13 Aug, 2019 2 commits
- Cleanup in HWQ example (remove stuff moved to libraries). · 66d82e37
  Rodolphe Lepigre authored Aug 14, 2019
  
  66d82e37
- Bump Iris. · 60001769
  Robbert Krebbers authored Aug 13, 2019
  
  60001769
13 Jul, 2019 1 commit
- more logatom case studies · 3f33781f
  Ralf Jung authored Jul 13, 2019
  
  3f33781f
11 Jul, 2019 2 commits
- remove SearchAbout · 193241d0
  Ralf Jung authored Jul 11, 2019
  
  193241d0
- Merge branch 'master' into 'master' · a58a15e2
  Ralf Jung authored Jul 11, 2019
```
Continuation change, extract_proph_winner change

See merge request iris/examples!26
```
  a58a15e2