Commits · robbert/big_sepM2 · Dan Frumin / iris-coq

Mar 29, 2019
- `nil` -> `empty` for some big_ops · 8c367063
  Dan Frumin authored 5 years ago
  
  8c367063
- A no-brainer generalization for big_sepM_2_later · aeae16a2
  Dan Frumin authored 5 years ago
  
  aeae16a2
- Proofmode stuff for big_sepM2. · a5753b1b
  Dan Frumin authored 5 years ago
  
  a5753b1b
- Add sbi lemmas for big_sepM2. · 7b9f1cb2
  Dan Frumin authored 5 years ago
  
  7b9f1cb2
- address some comments by @robbertkrebbers · 8d92dce3
  Dan Frumin authored 5 years ago
  
  8d92dce3
Mar 27, 2019
- Add big_sepM2_lookup_{1,2} · 3d56865d
  Dan Frumin authored 5 years ago
  
  3d56865d
- Simpler proof of `big_sepM2_lookup_acc`. · a1d6944f
  Dan Frumin authored 5 years ago
  
  a1d6944f
- Bump std++ · 0c77287c
  Dan Frumin authored 5 years ago
  
  0c77287c
- Implement big_sepM2 lemmas. · 6af84c02
  Dan Frumin authored 6 years ago
  
  6af84c02
- big_sepM2. · ccf2807f
  Robbert Krebbers authored 6 years ago and Dan Frumin committed 5 years ago
  
  ccf2807f
Mar 26, 2019
- Merge branch 'prophecy_list' into 'master' · 0495f119
  Ralf Jung authored 6 years ago
  
  Prophecy variables with lists See merge request iris/iris!225
  0495f119
Mar 22, 2019
- Style updates suggested by @robbertkrebbers · d479c851
  Rodolphe Lepigre authored 6 years ago
  
  d479c851
- Merge branch 'resolve_proph_fix' into 'master' · 9936cb12
  Ralf Jung authored 6 years ago
  
  Remove unnecessary arguments from `ResolveProphS`. See merge request iris/iris!227
  9936cb12
- Generalization suggested by @dfrumin · 40da12c2
  Rodolphe Lepigre authored 6 years ago
  
  40da12c2
Mar 20, 2019
- Remove unnecessary arguments from `ResolveProphS`. · 5e9a8aed
  Dan Frumin authored 6 years ago
  
  5e9a8aed
- Merge branch 'very_important_renaming' into 'master' · ac6dc97b
  Ralf Jung authored 6 years ago
  
  Rename bi/lib/counter_examples to bi/lib/counterexamples. See merge request iris/iris!226
  ac6dc97b
- Rename bi/lib/counter_examples to bi/lib/counterexamples. · 5c756fec
  Janno authored 6 years ago and Janno committed 6 years ago
  
  5c756fec
Mar 19, 2019
- Apply changes requested by @jung · d9402cba
  Rodolphe Lepigre authored 6 years ago
  
  d9402cba
- tweaks · 56f311a9
  Ralf Jung authored 6 years ago and Rodolphe Lepigre committed 6 years ago
  
  56f311a9
- Prophecy variables with lists. · b16b9f33
  Rodolphe Lepigre authored 6 years ago
  
  b16b9f33
Mar 17, 2019
- emphasize picking the right job name · 82e7e2ef
  Ralf Jung authored 6 years ago
  
  82e7e2ef
Mar 16, 2019
- Bump stdpp. · 6aed7177
  Robbert Krebbers authored 6 years ago
  
  6aed7177
Mar 15, 2019
- tweak COQTEST output · 7cd65053
  Ralf Jung authored 6 years ago
  
  7cd65053
- make NO_TEST=1 skips the tests · 46944241
  Ralf Jung authored 6 years ago
  
  46944241
- Bump stdpp. · 33ee70bf
  Robbert Krebbers authored 6 years ago
  
  33ee70bf
Mar 14, 2019
- Bump stdpp. · 2d1c8352
  Robbert Krebbers authored 6 years ago
  
  2d1c8352
- Merge branch 'robbert/kill_locked_value_lambdas' into 'master' · 66a69b0a
  Robbert Krebbers authored 6 years ago
  
  Get rid of locked value lambdas See merge request iris/iris!223
  66a69b0a
- Add CHANGELOG entry. · ac62dc3e
  Robbert Krebbers authored 6 years ago
  
  ac62dc3e
- Get rid of locked value lambdas. · ece1ecdd
  Robbert Krebbers authored 6 years ago
  
  ece1ecdd
- Update URL. · 2030d90c
  Robbert Krebbers authored 6 years ago
  
  2030d90c
- explain how to time a change against a reverse dependency · 3b9762bb
  Ralf Jung authored 6 years ago
  
  3b9762bb
Mar 13, 2019
- Merge branch 'ralf/doc' into 'master' · f31dc3c7
  Ralf Jung authored 6 years ago
  
  add documentation of the global RA pattern See merge request iris/iris!222
  f31dc3c7
- add documentation of the global RA pattern · 7f548a31
  Ralf Jung authored 6 years ago
  
  7f548a31
Mar 07, 2019
- Clean up `greatest_fixpoint_ne_outer`. · aaf0cfe3
  Robbert Krebbers authored 6 years ago
  
  aaf0cfe3
- Make proof of `least_fixpoint_unfold_2` more readable by including a `simple`. · b624d134
  Robbert Krebbers authored 6 years ago
  
  b624d134
- Propers for fixpoints. · 3f66477c
  Robbert Krebbers authored 6 years ago
  
  3f66477c
- mention the connection to ultrametric spaces · c8578f92
  Ralf Jung authored 6 years ago
  
  c8578f92
- Merge branch 'robbert/bupd_alt' into 'master' · a5771292
  Robbert Krebbers authored 6 years ago
  
  Alternative definition of the basic update modality See merge request iris/iris!211
  a5771292
Mar 06, 2019
- be more explicit about quantification order · f5d03e25
  Ralf Jung authored 6 years ago
  
  f5d03e25
- Merge branch 'master' of gitlab.mpi-sws.org:iris/iris into master.2 · 032f365f
  Ralf Jung authored 6 years ago
  
  032f365f