Commits · 60405a8a6b61845ddc5e0cf309dc88ffbc16e09f · Paolo G. Giarrusso / examples

Mar 13, 2020
- fill in blanks in LICENSE · 60405a8a
  Ralf Jung authored 5 years ago
  
  60405a8a
- Fix camera `cntCmra` to use `ZO`. · 64aa3577
  Robbert Krebbers authored 5 years ago
  
  `LeibnizO` should only be used for `Canonical Structure` declarations.
  64aa3577
- update dependencies, fix TCs unfolding more than before · d768c93d
  Ralf Jung authored 5 years ago
  
  d768c93d
Mar 11, 2020
- update dependencies · 2aa0b58c
  Ralf Jung authored 5 years ago
  
  2aa0b58c
Feb 23, 2020
- Bump Iris (array changes). · bd126535
  Robbert Krebbers authored 5 years ago
  
  bd126535
Feb 19, 2020
- Revert "temporarily switch nightly job to 8.11.0" · 1f96e762
  Ralf Jung authored 5 years ago
  
  This reverts commit 1a09032f. It doesn't help.
  1f96e762
- fix URL · a70ac5b1
  Ralf Jung authored 5 years ago
  
  a70ac5b1
- temporarily switch nightly job to 8.11.0 · 1a09032f
  Ralf Jung authored 5 years ago
  
  1a09032f
Feb 15, 2020
- bump Iris · 1ddda46e
  Ralf Jung authored 5 years ago
  
  1ddda46e
Feb 11, 2020
- bump to Coq 8.11 · eac03c6a
  Ralf Jung authored 5 years ago
  
  eac03c6a
Feb 02, 2020
- Bump Iris (`iSpecialize` changes). · 64380b40
  Robbert Krebbers authored 5 years ago
  
  64380b40
Jan 13, 2020
- upgrade to opam 2 · 92275f5b
  Ralf Jung authored 5 years ago
  
  92275f5b
- Small consistency fixes logrel heaplang. · b73553f9
  Robbert Krebbers authored 5 years ago
  
  b73553f9
Dec 13, 2019
- now this should work on 8.10 as well... sigh · e5b6840b
  Ralf Jung authored 5 years ago
  
  e5b6840b
- Mostly revert the previous commit · ace0db94
  Ralf Jung authored 5 years ago
  
  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 5 years ago
  
  5726c91c
- fix the rest of the repo for Coq 8.11 · 89196687
  Ralf Jung authored 5 years ago
  
  89196687
- make logatom work with Coq 8.11 · ea928791
  Ralf Jung authored 5 years ago
  
  ea928791
- nightly test for 8.11 branch · 5fa6ed80
  Ralf Jung authored 5 years ago
  
  5fa6ed80
Nov 21, 2019
- remove prophecy erasure proof (it is in the main Iris repo now) · b19a5b84
  Ralf Jung authored 5 years ago
  
  b19a5b84
- Bump Iris (`iPoseProof` changes). · de6dd885
  Robbert Krebbers authored 5 years ago
  
  de6dd885
Nov 14, 2019
- Merge branch 'rdcss_meta_token' into 'master' · a20140b8
  Ralf Jung authored 5 years ago
  
  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 5 years ago and Ralf Jung committed 5 years ago
  
  (and some cleanup)
  bbf33b66
Nov 13, 2019
- fix comment · d731cb31
  Ralf Jung authored 5 years ago
  
  d731cb31
- Merge branch 'rdcss_comment' into 'master' · 815b0180
  Ralf Jung authored 5 years ago
  
  Comment in the RDCSS spec about GClocs. See merge request iris/examples!29
  815b0180
- Expand RDCSS comments · 6639940c
  Rodolphe Lepigre authored 5 years ago and Ralf Jung committed 5 years ago
  
  6639940c
Nov 12, 2019
- Merge branch 'typed_proph' into 'master' · 8de152b1
  Ralf Jung authored 5 years ago
  
  Typed prophecy variables + cleanup See merge request iris/examples!28
  8de152b1
- Typed prophecy variables + cleanup · 0c551f14
  Rodolphe Lepigre authored 5 years ago and Ralf Jung committed 5 years ago
  
  0c551f14
- Bump iris (no changes needed) · f2637250
  Ralf Jung authored 5 years ago
  
  f2637250
Nov 07, 2019
- Bump Iris. · 3092552d
  Robbert Krebbers authored 5 years ago
  
  3092552d
- Merge branch 'ci/amin/fix-logrell-soundness' into 'master' · dd32b1ff
  Ralf Jung authored 5 years ago
  
  Fix logrel soundness proofs See merge request iris/examples!27
  dd32b1ff
- Fix logrel soundness proofs · b95a80e0
  Amin Timany authored 5 years ago and Ralf Jung committed 5 years ago
  
  b95a80e0
- link to opam repo commits for version numbers · a83f57e6
  Ralf Jung authored 5 years ago
  
  a83f57e6
- rely on the new ocaml default · 53fab07f
  Ralf Jung authored 5 years ago
  
  53fab07f
- fix ocaml version · f2c53bf9
  Ralf Jung authored 5 years ago
  
  f2c53bf9
- switch CI to Coq 8.10.1 · f8f664fe
  Ralf Jung authored 5 years ago
  
  f8f664fe
- update Makefile · 9612d208
  Ralf Jung authored 5 years ago
  
  9612d208
Nov 06, 2019
- and another 8.10 warning · 87ff31e9
  Ralf Jung authored 5 years ago
  
  87ff31e9
Nov 02, 2019
- bump Iris for LitErased -> LitPoison rename · 0c1aa0a0
  Ralf Jung authored 5 years ago
  
  0c1aa0a0
- warnings management · 034e63b6
  Ralf Jung authored 5 years ago
  
  034e63b6