Commits · 304a59013525299c0c6c6ec8ca4dbe4ca7ebd4c4 · Simon Spies / lambda-rust

Feb 23, 2017
- Remove a file from _Coqproject. · 304a5901
  Jacques-Henri Jourdan authored 8 years ago
  
  304a5901
- Define the type option. Merge some examples in this file. · e412af58
  Jacques-Henri Jourdan authored 8 years ago
  
  e412af58
Feb 22, 2017
- bump Iris · 22f5cdcd
  Ralf Jung authored 8 years ago
  
  22f5cdcd
- try to improve parallelism by putting the examples last · 999ce2e3
  Ralf Jung authored 8 years ago
  
  999ce2e3
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 5cfff714
  Ralf Jung authored 8 years ago
  
  5cfff714
- remove lft_ctx from subtype and eqtype · 3adf6cfd
  Ralf Jung authored 8 years ago
  
  3adf6cfd
- 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

Jacques-Henri Jourdan authored 8 years ago

* Also, removed the box from the definition of typing judgments, so that we can frame resources around them.

42f3528f

Feb 17, 2017

Make (most of) the typing lemmas implications in Iris. · 41044564

Jacques-Henri Jourdan authored 8 years ago

This requires using iApply instead of eapply to use them.

TODO : have an Iris version of Forall2, so that the lemmas for typing switches can be implications in Iris.

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
  
  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