Commits · fast_string · Simon Spies / lambda-rust · GitLab

Snippets Groups Projects

Feb 22, 2017
- Use fast_string. · 674b22d2
  Robbert Krebbers authored 8 years ago
  
  674b22d2
- Bump Iris. · 25c37eb0
  Robbert Krebbers authored 8 years ago
  
  25c37eb0
Feb 21, 2017
- RefCell: add comments explaining the data layout · 7f20c471
  Ralf Jung authored 8 years ago
  
  7f20c471
Feb 19, 2017
- Map for refmut. · da5a7b83
  Jacques-Henri Jourdan authored 8 years ago
  
  da5a7b83
Feb 18, 2017
- Map for Ref. · 42f3528f
  Jacques-Henri Jourdan authored 8 years ago
  42f3528f
Feb 17, 2017
- Make (most of) the typing lemmas implications in Iris. · 41044564
  Jacques-Henri Jourdan authored 8 years ago
  41044564
Feb 16, 2017
- Oops, forgot to bump Iris. · c0757d53
  Robbert Krebbers authored 8 years ago
  
  c0757d53
- Use Iris' iso_ofe infrastructure for types and seal off equiv and dist. · ce54063e
  Robbert Krebbers authored 8 years ago
  
  ce54063e
Feb 15, 2017
- Bump Iris version and make use of improved solve_ndisj. · 98be0049
  Robbert Krebbers authored 8 years ago
  
  98be0049
- 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
  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