Commits · 37e03ceb5ab305a64ff5aa4e296cde7daa2b8185 · Iris / stdpp

Aug 31, 2020
- Add lemmas and max for Qp · e16d8113
  Simon Friis Vindum authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  e16d8113
Jul 16, 2020

Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`, · 5710f90e

and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.

This was pointed out by @atrieu in !175 (comment 53746)

5710f90e

Jul 15, 2020
- add .0 in changelog for consistency · 048ade3d
  Ralf Jung authored 4 years ago
  
  048ade3d
- release std++ 1.4 · b26e5a4a
  Ralf Jung authored 4 years ago
  
  b26e5a4a
- CHANGELOG entry for !169 . · 76b66f20
  Robbert Krebbers authored 4 years ago
  
  76b66f20
- add author names to changelog · ab7ed0b8
  Ralf Jung authored 4 years ago
  
  ab7ed0b8
Jul 14, 2020
- edit and fix changelog · 8b8653b8
  Ralf Jung authored 4 years ago
  
  8b8653b8
Jul 02, 2020
- drop support for Coq 8.7 · 852e6fa7
  Ralf Jung authored 4 years ago
  
  852e6fa7
Jun 25, 2020
- CHANGELOG. · f4269240
  Robbert Krebbers authored 4 years ago
  
  f4269240
May 12, 2020
- rename Z2Nat_inj_div and Z2Nat_inj_mod · 0eaae21d
  Michael Sammler authored 4 years ago
  
  0eaae21d
- Revert "Merge branch 'byte-countable' into 'master'" · e99804d9
  Robbert Krebbers authored 4 years ago
  
  This reverts merge request !155
  e99804d9
- Add Countable instances for byte · 5346dd70
  Tej Chajed authored 4 years ago
  
  5346dd70
- CHANGELOG entry. · e6b17ca4
  Robbert Krebbers authored 4 years ago
  
  e6b17ca4
- Added rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions · a613b693
  Michael Sammler authored 4 years ago
  
  a613b693
Apr 30, 2020
- Add Countable instance for Ascii.ascii · bb75eecc
  Tej Chajed authored 4 years ago
  
  bb75eecc
Apr 16, 2020
- Added select and select_revert tactics · 199d011d
  Michael Sammler authored 4 years ago
  
  199d011d
Apr 15, 2020
- Extracted list_numbers.v with seq, seqZ, sum_list and max_list · fdd98ed8
  Michael Sammler authored 4 years ago
  
  fdd98ed8
Apr 11, 2020
- Add `encode_Z` function to encode element of countable type as `Z`. · 94b04a14
  Robbert Krebbers authored 4 years ago
  
  94b04a14
Apr 07, 2020
- CHANGELOG. · 85fb9ae4
  Robbert Krebbers authored 4 years ago
  
  85fb9ae4
Apr 06, 2020
- add missing sed flag · fd5a2ff5
  Ralf Jung authored 4 years ago
  
  fd5a2ff5
Apr 03, 2020
- Rename `fin_maps.singleton_proper` into `singletonM_proper`. · 59444525
  Robbert Krebbers authored 4 years ago
  
  59444525
Apr 02, 2020
- adjust to GNU sed · 809acb6d
  Ralf Jung authored 4 years ago
  
  809acb6d
Mar 31, 2020
- Fix typo in CHANGELOG · a75f766b
  Tej Chajed authored 4 years ago
  
  Rename performed in !131 was on drop_insert, not drop_length
  a75f766b
- random collection of lemmas · ef163e26
  Michael Sammler authored 5 years ago
  
  ef163e26
Mar 19, 2020
- add sed script for 1.3.0 · 1eaa5cf6
  Ralf Jung authored 5 years ago
  
  1eaa5cf6
Mar 17, 2020
- Update CHANGELOG for 1.3 release. · 731caa8a
  Robbert Krebbers authored 5 years ago
  
  731caa8a
- CHANGELOG. · 6b11b096
  Robbert Krebbers authored 5 years ago
  
  6b11b096
- More CHANGELOG. · 97079040
  Robbert Krebbers authored 5 years ago
  
  97079040
- CHANGELOG. · f05baf13
  Robbert Krebbers authored 5 years ago
  
  f05baf13
Mar 10, 2020
- Set `Hint Mode` for logical `TCX` type classes. · b130764f
  Robbert Krebbers authored 5 years ago
  
  b130764f
Mar 09, 2020
- Add tactic `set_unfold in H`. · bd0e6352
  Robbert Krebbers authored 5 years ago
  
  bd0e6352
Mar 05, 2020
- Rename `fin_of_nat` → `nat_to_fin` to follow the conventions. · 9b4ce6dd
  Robbert Krebbers authored 5 years ago
  
  9b4ce6dd
Feb 28, 2020
- Changelog entry · 4f00de71
  Armaël Guéneau authored 5 years ago
  
  4f00de71
Feb 24, 2020
- CHANGELOG entry. · 2d2a72ae
  Robbert Krebbers authored 5 years ago
  
  2d2a72ae
- CHANGELOG entry. · 8e949e3c
  Robbert Krebbers authored 5 years ago
  
  8e949e3c
Feb 17, 2020
- CHANGELOG entry. · ab51e3fd
  Robbert Krebbers authored 5 years ago
  
  ab51e3fd
Oct 01, 2019
- Generalize `list_find` lemmas to become bi-implications. · 69c36292
  Robbert Krebbers authored 5 years ago
  
  Thanks to @jules for the suggestion and an initial proof.
  69c36292
Sep 19, 2019
- CHANGELOG entry. · 3a1f5195
  Robbert Krebbers authored 5 years ago
  
  3a1f5195
Sep 11, 2019
- Equality lemma for `dom D (filter P m)`. · 16da535d
  Robbert Krebbers authored 5 years ago
  
  16da535d
Aug 29, 2019
- release 1.2.1 · 75435486
  Ralf Jung authored 5 years ago
  
  coq-stdpp-1.2.1
  
  75435486