Commits · f9ee8400573d7b100ae1f727eca5d248d55d155f · Iris / stdpp

Aug 08, 2022
- Merge branch 'msammler/more_1_2_lemmas' into 'master' · f9ee8400
  Robbert Krebbers authored 2 years ago
  
  Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None See merge request !405
  f9ee8400
- Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None · 05c58b27
  Michael Sammler authored 2 years ago
  
  05c58b27
Aug 03, 2022
- Merge branch 'ci/msammler/lookup_union_l' into 'master' · b99e79cf
  Robbert Krebbers authored 2 years ago
  
  Add lookup_union_l' See merge request !395
  b99e79cf
- Rename lookup_union_l' to lookup_union_l and add lookup_union_l dual to lookup_union_r · 8288632b
  Michael Sammler authored 2 years ago
  
  8288632b
Aug 01, 2022
- Merge branch 'ci/msammler/map_agree' into 'master' · beee46c8
  Robbert Krebbers authored 2 years ago
  
  Add map_agree See merge request !392
  beee46c8
- Add CHANGELOG · 05281d98
  Michael Sammler authored 2 years ago
  
  05281d98
- Tweak some proofs. · c0f8d45c
  Robbert Krebbers authored 2 years ago and Michael Sammler committed 2 years ago
  
  c0f8d45c
- Add map_agree · ad2023ed
  Michael Sammler authored 2 years ago
  
  ad2023ed
- Merge branch 'robbert/map_disjoint_fmap' into 'master' · 6f1ca045
  Robbert Krebbers authored 2 years ago
  
  Flip direction of `map_disjoint_fmap`. See merge request !398
  6f1ca045
- CHANGELOG. · 9198e66b
  Robbert Krebbers authored 2 years ago
  
  9198e66b
- Flip direction of `map_disjoint_fmap`. · 7ef1770c
  Robbert Krebbers authored 2 years ago
  
  7ef1770c
- Merge branch 'ci/msammler/list_subseteq_dec' into 'master' · 9d78117d
  Robbert Krebbers authored 2 years ago
  
  Add list_subseteq_dec See merge request !400
  9d78117d
- Add list_subseteq_dec · ef9d9dde
  Michael Sammler authored 2 years ago
  
  ef9d9dde
Jul 31, 2022
- Merge branch 'ci/msammler/map_commuting_lemmas' into 'master' · fd0deb99
  Robbert Krebbers authored 2 years ago
  
  Add lookup lemmas for partial alter and commuting lemmas for alter See merge request !399
  fd0deb99
- Avoid relying on `setoid_rewrite` unfolding things. · bfa786c0
  Robbert Krebbers authored 2 years ago
  
  bfa786c0
- Merge branch 'ci/msammler/join_length' into 'master' · 7915ff75
  Robbert Krebbers authored 2 years ago
  
  Add join_length See merge request !401
  7915ff75
Jul 27, 2022
- Add join_length · d5e8449a
  Michael Sammler authored 2 years ago
  
  d5e8449a
- Add lookup lemmas for partial alter and commuting lemmas for alter · 20cfcd95
  Michael Sammler authored 2 years ago
  
  20cfcd95
- Merge branch 'ci/msammler/case_match_eqn' into 'master' · 3897126a
  Robbert Krebbers authored 2 years ago
  
  Add case_match eqn: tactic for naming hypotheses generated by case_match See merge request !388
  3897126a
- Add case_match eqn: tactic for naming hypotheses generated by case_match · a6f215a9
  Michael Sammler authored 2 years ago
  
  a6f215a9
- Merge branch 'ci/msammler/map_Exists' into 'master' · ba7cf37b
  Robbert Krebbers authored 2 years ago
  
  Add map_Exists See merge request !390
  ba7cf37b
- Add CHANGELOG for `map_Exists` · 3ebfb878
  Michael Sammler authored 2 years ago
  
  3ebfb878
- Add `map_Exists_ind`. · 457abb83
  Robbert Krebbers authored 2 years ago and Michael Sammler committed 2 years ago
  
  457abb83
- Add `map_Exists_lookup_{1,2}`. · ff92006d
  Robbert Krebbers authored 2 years ago and Michael Sammler committed 2 years ago
  
  ff92006d
- Add map_Exists · 183bc449
  Michael Sammler authored 2 years ago
  
  183bc449
Jul 26, 2022
- Merge branch 'ci/msammler/kmap_subseteq' into 'master' · 224790c8
  Robbert Krebbers authored 2 years ago
  
  Fix the naming of kmap_subseteq and kmap_subset See merge request !393
  224790c8
- Merge branch 'ci/msammler/list_lookup_imap_Some' into 'master' · 13c91b69
  Robbert Krebbers authored 2 years ago
  
  Add list_lookup_imap_Some See merge request !396
  13c91b69
- Merge branch 'ci/msammler/omap_app' into 'master' · a7858376
  Robbert Krebbers authored 2 years ago
  
  Add list_fmap_delete, omap_app, and omap_option_list See merge request !397
  a7858376
- Fix the naming of kmap_subseteq and kmap_subset · 10d41e4e
  Michael Sammler authored 2 years ago
  
  10d41e4e
- Add list_lookup_imap_Some · 0ffb8c12
  Michael Sammler authored 2 years ago
  
  0ffb8c12
- Add list_fmap_delete, omap_app, and omap_option_list · 7403ff94
  Michael Sammler authored 2 years ago
  
  7403ff94
Jul 18, 2022
- Fix broken comment. · 68f6f9cf
  Robbert Krebbers authored 2 years ago
  
  68f6f9cf
Jul 07, 2022
- remove a useless auto · e847956f
  Ralf Jung authored 2 years ago
  
  e847956f
- Merge branch 'eauto-cost' into 'master' · ad402fb2
  Ralf Jung authored 2 years ago
  
  prepare for https://github.com/coq/coq/pull/16289 See merge request iris/stdpp!385
  ad402fb2
- prepare for https://github.com/coq/coq/pull/16289 · 315fcfab
  Andrej Dudenhefner authored 2 years ago
  
  315fcfab
Jun 28, 2022
- avoid section variables for real · 45fd520d
  Ralf Jung authored 2 years ago
  
  45fd520d
Jun 27, 2022
- avoid section variables in printed terms · c4055887
  Ralf Jung authored 2 years ago
  
  c4055887
- adjust regexp · 0a010579
  Ralf Jung authored 2 years ago
  
  0a010579
- normalize away new section variable info · 2b12b6fd
  Ralf Jung authored 2 years ago
  
  2b12b6fd
Jun 08, 2022
- ref tests: be less sensitive to trailing spaces · 4f82f462
  Ralf Jung authored 2 years ago
  
  4f82f462