Commits · 6bb1fc01275068429f0782ed0dab16040c6af81c · Iris / stdpp

Sep 28, 2024
- Enable `map_Forall2` to be used in nested inductive relations. · 6bb1fc01
  Robbert Krebbers authored 5 months ago
  
  6bb1fc01
Sep 11, 2024
- sync dune flags · bc4fce09
  Ralf Jung authored 6 months ago
  
  bc4fce09
- Merge branch 'robbert/deprecate_rev_length' into 'master' · 6a0896a2
  Ralf Jung authored 6 months ago
  
  Unsilence deprecation warning regarding list lemmas. See merge request !574
  6a0896a2
- move COQ_REF further up so it is easier to see · d297a432
  Ralf Jung authored 6 months ago
  
  d297a432
- Unsilence deprecation warning regarding list lemmas. · 2db35c48
  Robbert Krebbers authored 6 months ago
  
  2db35c48
- test coq 8.19.1 · 8a031c06
  Ralf Jung authored 6 months ago
  
  8a031c06
- switch reftesting to Coq 8.20 · f894e0cf
  Ralf Jung authored 6 months ago
  
  f894e0cf
- silence another warning · f6973baf
  Ralf Jung authored 6 months ago
  
  f6973baf
- silence Coq 8.20 deprecation warnings · 21aaa5d3
  Ralf Jung authored 6 months ago
  
  21aaa5d3
- test Coq 8.20 · 5da2f2e2
  Ralf Jung authored 6 months ago
  
  5da2f2e2
Sep 10, 2024
- Merge branch 'robbert/set_fold_union' into 'master' · a1a12e00
  Robbert Krebbers authored 6 months ago
  
  Add `set_fold_union_strong` and similarly for map See merge request !417
  a1a12e00
- Comments. · 8bfd5a08
  Robbert Krebbers authored 6 months ago
  
  8bfd5a08
- CHANGELOG. · 919f61f7
  Robbert Krebbers authored 6 months ago
  
  919f61f7
- Also add union lemmas for `map_fold`. · 94ea2e33
  Robbert Krebbers authored 6 months ago
  
  94ea2e33
- Add lemmas `set_fold_union_strong` and `set_fold_union`. · c0b1ec66
  Robbert Krebbers authored 2 years ago
  
  c0b1ec66
- Add lemma `foldr_idemp`. · 47a3477b
  Robbert Krebbers authored 2 years ago
  
  47a3477b
- Merge branch 'robbert/string_notation' into 'master' · bc76f1d5
  Robbert Krebbers authored 6 months ago
  
  Better use of modules / less global polution for strings See merge request !570
  bc76f1d5
- Tweak CHANGELOG. · 1dd6bcab
  Robbert Krebbers authored 6 months ago
  
  1dd6bcab
- CHANGELOG. · 420bd785
  Robbert Krebbers authored 6 months ago
  
  420bd785
- Add order on strings. · 560412f0
  Robbert Krebbers authored 6 months ago
  
  560412f0
- Better use of modules for string, consistent with numbers. · c8de231b
  Robbert Krebbers authored 6 months ago
  
  c8de231b
- Merge branch 'robbert/foldr_cons_permute' into 'master' · 2a3b41ca
  Robbert Krebbers authored 6 months ago
  
  Make `foldr_cons_permute` lemmas consistent. See merge request !573
  2a3b41ca
- Merge branch 'robbert/map_Forall2_dom' into 'master' · fb7a1e04
  Ralf Jung authored 6 months ago
  
  Add `map_Forall2_dom`. See merge request !569
  fb7a1e04
Sep 08, 2024
- CHANGELOG. · cf6aa554
  Robbert Krebbers authored 6 months ago
  
  cf6aa554
- Make `foldr_cons_permute` lemmas consistent. · cb463d4f
  Robbert Krebbers authored 6 months ago
  
  cb463d4f
- Merge branch 'paolo/qed-decision' into 'master' · d37b5e70
  Robbert Krebbers authored 6 months ago
  
  numbers.v: Don't Qed Decision instances See merge request !572
  d37b5e70
- new line · ffb2184e
  Robbert Krebbers authored 6 months ago
  
  ffb2184e
Sep 07, 2024
- numbers.v: avoid Qed'ing Decision instances · 1af28e21
  Paolo G. Giarrusso authored 6 months ago
  
  1af28e21
- numbers.v: use abstract more to split Decision instances by proof-relevance · fcceace4
  Paolo G. Giarrusso authored 6 months ago
  
  fcceace4
Sep 06, 2024
- Merge branch 'robbert/sorted_unique' into 'master' · 9d0f527a
  Robbert Krebbers authored 6 months ago
  
  Stronger sorted unique lemmas See merge request !567
  9d0f527a
- Add variants of `Sorted_unique` that only require anti symmetry for the... · 1d6ec7e6
  Robbert Krebbers authored 6 months ago
  
  Add variants of `Sorted_unique` that only require anti symmetry for the elements that are in the list.
  1d6ec7e6
- Merge branch 'robbert/string_notation' into 'master' · 1844a78e
  Ralf Jung authored 6 months ago
  
  Notation for string literals in `stdpp_scope`. See merge request !568
  1844a78e
- Add `map_Forall2_dom`. · 83c6c5eb
  Robbert Krebbers authored 6 months ago
  
  83c6c5eb
- Test cases for string notation. · 1c845125
  Robbert Krebbers authored 6 months ago
  
  1c845125
- CHANGELOG. · 0e631f7f
  Robbert Krebbers authored 6 months ago
  
  0e631f7f
- Notation for string literals in `stdpp_scope`. · bf1ad734
  Robbert Krebbers authored 6 months ago
  
  bf1ad734
Sep 04, 2024
- Merge branch 'robbert/map_fold_ind' into 'master' · 80267a5e
  Robbert Krebbers authored 6 months ago
  
  Stronger induction principle for `map_fold`. See merge request !566
  80267a5e
- Improve CHANGELOG. · d17140b8
  Robbert Krebbers authored 6 months ago
  
  d17140b8
- Coding style. · d338c042
  Robbert Krebbers authored 6 months ago
  
  d338c042
- CHANGELOG. · 70f3e338
  Robbert Krebbers authored 6 months ago
  
  70f3e338