Commits · 0710439b2f4f24010e222c9d620b75790e6f98c3 · Iris / stdpp

Jan 20, 2021
- fmt · 0710439b
  Ralf Jung authored 4 years ago
  
  0710439b
- add rename-by-pattern tactic · 609de3aa
  Ralf Jung authored 4 years ago
  
  609de3aa
Jan 19, 2021
- Merge branch 'robbert/omega' into 'master' · 96cb4bc9
  Ralf Jung authored 4 years ago
  
  Remove hint db and import of omega, since omega will be removed from Coq. See merge request !216
  96cb4bc9
- Merge branch 'ci/ralf/warnings' into 'master' · e394bc6b
  Robbert Krebbers authored 4 years ago
  
  fix and reject warnings on Coq 8.13 See merge request !214
  e394bc6b
- Merge branch 'ralf/zip-diag' into 'master' · 89825de7
  Robbert Krebbers authored 4 years ago
  
  add zip_with_diag and zip_diag See merge request !215
  89825de7
- CHANGELOG. · de22a852
  Robbert Krebbers authored 4 years ago
  
  de22a852
- Remove hint db and import of omega, since omega will be removed from Coq. · 1c2e6891
  Robbert Krebbers authored 4 years ago
  
  See https://github.com/coq/coq/pull/13741#issuecomment-762761112
  1c2e6891
- add zip_with_diag and zip_diag · 8f69a159
  Ralf Jung authored 4 years ago
  
  8f69a159
- fix and reject warnings on Coq 8.13 · e7a7f588
  Ralf Jung authored 4 years ago
  
  e7a7f588
Jan 17, 2021
- Add lemmas `map_fmap_zip_with_{l,r}`. · fc52ac53
  Robbert Krebbers authored 4 years ago
  
  fc52ac53
Jan 15, 2021
- test on Coq 8.13.0 · 8407f2ca
  Ralf Jung authored 4 years ago
  
  8407f2ca
- Merge branch 'ralf/set_map' into 'master' · 6f8111e2
  Robbert Krebbers authored 4 years ago
  
  add set_map_union, set_map_singleton See merge request !213
  6f8111e2
- Apply 1 suggestion(s) to 1 file(s) · c4b14c58
  Ralf Jung authored 4 years ago
  
  c4b14c58
- add some singleton and snoc lemmas · 5e5b2d17
  Ralf Jung authored 4 years ago
  
  5e5b2d17
- add set_map_empty · e37b4e68
  Ralf Jung authored 4 years ago
  
  e37b4e68
- add set_map_union, set_map_singleton · bf59b1eb
  Ralf Jung authored 4 years ago
  
  bf59b1eb
Jan 13, 2021
- ref tests: normalize subgoal to goal · 616b4062
  Ralf Jung authored 4 years ago
  
  616b4062
Jan 11, 2021
- Shorten proof. · c5676b11
  Robbert Krebbers authored 4 years ago
  
  c5676b11
- Merge branch 'ralf/map-size' into 'master' · b55715d3
  Robbert Krebbers authored 4 years ago
  
  prove map_size_delete, map_size_insert_Some, map_to_list_delete See merge request !208
  b55715d3
- Merge branch 'ci/robbert/seq_S' into 'master' · 40135869
  Robbert Krebbers authored 4 years ago
  
  Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib See merge request !212
  40135869
- Fix compilation with Coq 8.10 (which has a weaker `lia`). · d7732dcb
  Robbert Krebbers authored 4 years ago
  
  d7732dcb
- Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib. · 9782eda9
  Robbert Krebbers authored 4 years ago
  
  9782eda9
- Merge branch 'ralf/list_numbers' into 'master' · 523920d1
  Robbert Krebbers authored 4 years ago
  
  upstream some list_numbers lemmas from Perennial See merge request !211
  523920d1
- add changelog entry · d80a55ce
  Ralf Jung authored 4 years ago
  
  d80a55ce
- simplify proofs (by Robbert) · c57fe844
  Ralf Jung authored 4 years ago
  
  c57fe844
- adjust map_size_delete statement · 83901f25
  Ralf Jung authored 4 years ago
  
  83901f25
- simplify proof (by Robbert) · c4875672
  Ralf Jung authored 4 years ago
  
  c4875672
- simplify proof (by Robbert) · c111795c
  Ralf Jung authored 4 years ago
  
  c111795c
- add seqZ_S · 794ce99a
  Ralf Jung authored 4 years ago
  
  794ce99a
- adjust variable names and remove redundant scope · 59b248ed
  Ralf Jung authored 4 years ago
  
  59b248ed
- rename seq_S_end_app -> seq_S_snoc · 8d8a0f0a
  Ralf Jung authored 4 years ago
  
  8d8a0f0a
- add elem_of_seq, elem_of_seqZ, seqZ_app · d5b1ae21
  Ralf Jung authored 4 years ago
  
  Proofs by Tej
  d5b1ae21
- Merge branch 'ralf/take_0' into 'master' · 77e40221
  Robbert Krebbers authored 4 years ago
  
  prove take_0 See merge request iris/stdpp!209
  77e40221
- prove take_0 · 3c4993d2
  Ralf Jung authored 4 years ago
  
  3c4993d2
- prove map_size_delete, map_size_insert_Some, map_to_list_delete · 65ddd0da
  Ralf Jung authored 4 years ago
  
  65ddd0da
Jan 08, 2021
- make sure all Instance/Argument/Hint are qualified · 3ae73218
  Ralf Jung authored 4 years ago
  
  3ae73218
Jan 07, 2021
- Merge branch 'ralf/explicit-local-global' into 'master' · 43aea848
  Robbert Krebbers authored 4 years ago
  
  explicit Local/Global for all Instance, Arguments, Hint See merge request iris/stdpp!207
  43aea848
- also adjust Hint · 3081c441
  Ralf Jung authored 4 years ago
  
  3081c441
- explicit Local/Global for all Instance and Arguments · 8709344e
  Ralf Jung authored 4 years ago
  
  8709344e
- Merge branch 'robbert/fmap_empty' into 'master' · df64edb2
  Robbert Krebbers authored 4 years ago
  
  Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... See merge request !205
  df64edb2