Commits · 3e2ae1fc9de20523d7c446c1992aaf3d2a0c8bb0 · Simon Spies / lambda-rust · GitLab

Snippets Groups Projects

Feb 15, 2017
- Bump Iris and fix stuff. · 3e2ae1fc
  Robbert Krebbers authored 8 years ago
  
  3e2ae1fc
- Port Iris 84d78426: Remove an Ltac hack that was there for unknown reason. · 41dd8385
  Robbert Krebbers authored 8 years ago
  
  41dd8385
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 855e5e45
  Ralf Jung authored 8 years ago
  
  855e5e45
- avoid using wp_bind; use wp_apply instead · c10260ac
  Ralf Jung authored 8 years ago
  
  c10260ac
- Remove uses of iStartProof, which is intended as being an internal tactic. · ec40350b
  Jacques-Henri Jourdan authored 8 years ago
  
  ec40350b
Feb 13, 2017
- Bump iris. Simplify some proofs. · 6d36b8cf
  Jacques-Henri Jourdan authored 8 years ago
  
  6d36b8cf
- refcell: split switching back to the type system and chekcing the first instruction into two steps · f4e566ec
  Ralf Jung authored 8 years ago
  
  f4e566ec
- update Cell to prove replace instead of just set (like in latest nightly Rust) · 0b73ab70
  Ralf Jung authored 8 years ago
  
  0b73ab70
Feb 12, 2017
- Bump Iris and remove a FIXME. · 9aeb8f2b
  Robbert Krebbers authored 8 years ago
  
  9aeb8f2b
- Remove another FIXME. · 3c5e3622
  Robbert Krebbers authored 8 years ago
  
  3c5e3622
Feb 11, 2017
- Bump Iris and fix several TODOs and FIXMEs. · f1f3836d
  Robbert Krebbers authored 8 years ago
  
  f1f3836d
- update lang to use heap_lang style: merge lifting.v and derived.v · 53a237b5
  Ralf Jung authored 8 years ago
  
  53a237b5
- show join_handle_subtype inside the logic · 8ba197a1
  Ralf Jung authored 8 years ago
  
  8ba197a1
- allow subtyping for join_handle · cf7f3ffc
  Ralf Jung authored 8 years ago
  
  cf7f3ffc
- note a TODO · 3c6d0d23
  Ralf Jung authored 8 years ago
  
  3c6d0d23
- type the join function · 3bf41e48
  Ralf Jung authored 8 years ago
  
  3bf41e48
Feb 10, 2017
- prove that spawn can return a join handle · 3b7a99c2
  Ralf Jung authored 8 years ago
  
  3b7a99c2
- wp_alloc provides a vector of allocated values · 4622cb39
  Ralf Jung authored 8 years ago
  
  4622cb39
- leave a TODO · 9edc1b15
  Ralf Jung authored 8 years ago
  
  9edc1b15
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 9b8d36ce
  Ralf Jung authored 8 years ago
  
  9b8d36ce
- adapt the locking approach for value-lambdas like we did in iris.heap_lang · 6dcf60e2
  Ralf Jung authored 8 years ago
  
  6dcf60e2
Feb 09, 2017
- Bumb Iris version. · a4e9ac66
  Robbert Krebbers authored 8 years ago
  
  a4e9ac66
- Remove obsolete TODO. · 87413b96
  Robbert Krebbers authored 8 years ago
  
  87413b96
- prove a spawn-join primitive · 7532af1b
  Ralf Jung authored 8 years ago
  
  The interface is slightly more flexible than the one on iris.heap_lang to support continuation passing style
  7532af1b
- update build system · b7247b08
  Ralf Jung authored 8 years ago
  
  b7247b08
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 3dd95b21
  Jacques-Henri Jourdan authored 8 years ago
  
  3dd95b21
- Iris master. · 36b7acc9
  Jacques-Henri Jourdan authored 8 years ago
  
  36b7acc9
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 108063ea
  Ralf Jung authored 8 years ago
  
  108063ea
- prove thread::spawn · 1d5970bd
  Ralf Jung authored 8 years ago
  
  1d5970bd
- improve function type notation · f6a263a8
  Ralf Jung authored 8 years ago
  
  f6a263a8
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 5682cfe0
  Jacques-Henri Jourdan authored 8 years ago
  
  5682cfe0
- update iris to use stdpp · 10b7a540
  Ralf Jung authored 8 years ago
  
  10b7a540
- update buildsystem · 7594024f
  Ralf Jung authored 8 years ago
  
  7594024f
Feb 08, 2017
- use new function type notation for examples · d5ab6f51
  Ralf Jung authored 8 years ago
  
  d5ab6f51
- notation for the function type · 052d9f00
  Ralf Jung authored 8 years ago
  
  052d9f00
- Cell::get_mut does not need the type to be copy · 22cd25ab
  Ralf Jung authored 8 years ago
  
  22cd25ab
Jan 30, 2017
- Dereferencing and dropping a RefMut. · 089b2cd3
  Jacques-Henri Jourdan authored 8 years ago
  
  089b2cd3
- Forgot to add two files. · 6c83f2c8
  Jacques-Henri Jourdan authored 8 years ago
  
  6c83f2c8
- Merge remote-tracking branch 'origin/master' · 2a0bc9c6
  Jacques-Henri Jourdan authored 8 years ago
  
  Also update wrt recent iris.
  2a0bc9c6
- dropping a ref. · 59c66c09
  Jacques-Henri Jourdan authored 8 years ago
  
  59c66c09