Commits · f0449ed6183a21c65a82f59efdba3120413e3cf4 · Iris / lambda-rust · GitLab

Snippets Groups Projects

Mar 05, 2017
- lrust_typing: make sum type opaque, for consistency with the other types · f0449ed6
  Ralf Jung authored 8 years ago
  
  f0449ed6
- fix comment in spawn.v · a0aa9ed3
  Ralf Jung authored 8 years ago
  
  a0aa9ed3
- Merge branch 'ralf/ci/box' into 'master' · 5d6f2eda
  Ralf Jung authored 8 years ago
  5d6f2eda
Mar 04, 2017
- Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into... · 03fdb63e
  Jacques-Henri Jourdan authored 8 years ago
  03fdb63e
- Make box a definition and prove it contractive · 9b92a3cf
  Ralf Jung authored 8 years ago
  9b92a3cf
Mar 03, 2017
- New notation : typed_val. · 955f8849
  Jacques-Henri Jourdan authored 8 years ago
  955f8849
Mar 01, 2017
- bump Iris · 003dcbdb
  Ralf Jung authored 8 years ago
  
  003dcbdb
- switch to new CI machine · 08170eab
  Ralf Jung authored 8 years ago
  
  08170eab
- forgot to bump Iris · e9941790
  Ralf Jung authored 8 years ago
  
  e9941790
- make join_handle a contractive type · d936baff
  Ralf Jung authored 8 years ago
  
  d936baff
- show all type-non-expansive functions to also be properly non-expansive · 15b9474e
  Ralf Jung authored 8 years ago
  
  15b9474e
- new fixpoint · d5d09dae
  Ralf Jung authored 8 years ago
  d5d09dae
Feb 28, 2017
- Clarify the API of shared borrows: create specific lemmas for lftN. · e6d43e1b
  Jacques-Henri Jourdan authored 8 years ago
  
  e6d43e1b
- Use the empty set for the mask of the closing update of borrows. · 82e10900
  Jacques-Henri Jourdan authored 8 years ago
  82e10900
Feb 25, 2017
- Proove that RWlock is safe. · e7e16b65
  Jacques-Henri Jourdan authored 8 years ago
  e7e16b65
- Cosmetic changes in refcell. · f4b638e7
  Jacques-Henri Jourdan authored 8 years ago
  
  f4b638e7
- Change the masks of shared borrows, so that the previous commit has a purpose. · adfeaec0
  Jacques-Henri Jourdan authored 8 years ago
  adfeaec0
Feb 24, 2017
- Make it possible to specify a namespace for shared borrows. · ca45ee8f
  Jacques-Henri Jourdan authored 8 years ago
  
  ca45ee8f
- Cosmetic changes in spawn.v. · 4a70e97b
  Jacques-Henri Jourdan authored 8 years ago
  
  4a70e97b
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
- 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