Commits · 9869a4f842adb9b1ca1bd68a51f63d1a2e703d7f · Tej Chajed / stdpp

01 Dec, 2021 4 commits
- add lemma `zip_with_take_both` · 9869a4f8
  Glen Mével authored Nov 23, 2021
  
  9869a4f8
- Fix formatting of bool_to_Z_spec · 77100af7
  Michael Sammler authored Dec 01, 2021
  
  77100af7
- Merge branch 'msammler/bool_to_Z' into 'master' · a457d6de
  Michael Sammler authored Dec 01, 2021
```
Add bool_to_Z

See merge request iris/stdpp!341
```
  a457d6de
- Add bool_to_Z · 08fecbf6
  Michael Sammler authored Nov 30, 2021
  
  08fecbf6
26 Nov, 2021 4 commits
- tweak CI settings · 18dd6ca9
  Ralf Jung authored Nov 26, 2021
  
  18dd6ca9
- switch CI to Coq 8.14.1 · 68fc5055
  Ralf Jung authored Nov 26, 2021
  
  68fc5055
- Merge branch 'msammler/mjoin_lookup' into 'master' · 85d36776
  Robbert Krebbers authored Nov 26, 2021
```
Lemmas for lookup on mjoin

See merge request iris/stdpp!340
```
  85d36776
- Lemmas for lookup on mjoin · 91936be2
  Michael Sammler authored Nov 25, 2021
  
  91936be2
24 Nov, 2021 4 commits
- Merge branch 'msammler/reverse_lookup_sublist_lookup' into 'master' · 82c4f583
  Robbert Krebbers authored Nov 24, 2021
```
Add reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_Some

See merge request iris/stdpp!338
```
  82c4f583
- Merge branch 'msammler/small-lemma-collection' into 'master' · c2bad317
  Robbert Krebbers authored Nov 24, 2021
```
Upstreaming a small collection of lemmas

See merge request iris/stdpp!337
```
  c2bad317
- Add reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_Some · 6d639468
  Michael Sammler authored Nov 24, 2021
  
  6d639468
- Upstreaming a small collection of lemmas · cb25928e
  Michael Sammler authored Nov 24, 2021
  
  cb25928e
23 Nov, 2021 2 commits
- Merge branch 'fix-coq-lint-macos' into 'master' · f370d2fe
  Ralf Jung authored Nov 23, 2021
```
Fix coq-lint.sh on macOS

See merge request iris/stdpp!336
```
  f370d2fe
- Make coq-lint.sh compatible with BSD grep · 7d7097a6
  Tej Chajed authored Nov 23, 2021
```
On macOS, egrep does not support empty subexpressions in a regex OR.
```
  7d7097a6
22 Nov, 2021 1 commit
- Merge branch 'robbert/map_subseteq_inv' into 'master' · 9765b5fe
  Robbert Krebbers authored Nov 22, 2021
```
Add lemma `map_subseteq_inv`.

See merge request iris/stdpp!335
```
  9765b5fe
18 Nov, 2021 1 commit
- Add lemma `map_subseteq_inv`. · 6df1a647
  Robbert Krebbers authored Nov 18, 2021
  
  6df1a647
15 Nov, 2021 2 commits
- fix coq-lint for Instances · 564dc692
  Ralf Jung authored Nov 15, 2021
  
  564dc692
- silence a warning we cannot fix any time soon · d856d6ea
  Ralf Jung authored Nov 15, 2021
  
  d856d6ea
13 Nov, 2021 2 commits
- Merge branch 'ralf/fail' into 'master' · 4df62327
  Ralf Jung authored Nov 13, 2021
```
normalize for Fail printing locations

See merge request iris/stdpp!334
```
  4df62327
- normalize for Fail printing locations · 5891312b
  Ralf Jung authored Nov 12, 2021
  
  5891312b
08 Nov, 2021 1 commit
- add missing last name · 0939f35d
  Ralf Jung authored Nov 08, 2021
  
  0939f35d
05 Nov, 2021 10 commits
- finalize release · 4922a992
  Ralf Jung authored Nov 05, 2021
  
  4922a992
- Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp · d9048e46
  Ralf Jung authored Nov 05, 2021
  
  d9048e46
- officially support 8.14.0 · 1bd19c8c
  Ralf Jung authored Nov 05, 2021
  
  1bd19c8c
- Merge branch 'release-notes-1.6.0' into 'master' · d888f8a7
  Ralf Jung authored Nov 05, 2021
```
std++ 1.6.0 release notes

Closes #119

See merge request !333
```
  d888f8a7
- std++ 1.6.0 release notes · 0e901502
  Tej Chajed authored Nov 05, 2021 and Ralf Jung committed Nov 05, 2021
  
  0e901502
- add logpath tag to opam file · 1304e178
  Ralf Jung authored Nov 05, 2021
  
  1304e178
- Merge branch 'choose_proper' into 'master' · ac0c4539
  Ralf Jung authored Nov 05, 2021
```
countable.v: prove choose_proper

See merge request !327
```
  ac0c4539
- fix changelog · 2f4644bf
  Robbert Krebbers authored Nov 05, 2021 and Ralf Jung committed Nov 05, 2021
  
  2f4644bf
- CHANGELOG: Unnest, and mention compatibility · c1d2615a
  Paolo G. Giarrusso authored Nov 05, 2021
  
  c1d2615a
- Extend changelog mentioning new `well_founded` module · afcea245
  Ralf Jung authored Nov 05, 2021 and Paolo G. Giarrusso committed Nov 05, 2021
  
  afcea245
04 Nov, 2021 1 commit
- CHANGELOG · 1e2df25e
  Paolo G. Giarrusso authored Nov 04, 2021
  
  1e2df25e
27 Oct, 2021 4 commits
- countable.v: prove choose_proper · 905203e1
  Paolo G. Giarrusso authored Oct 01, 2021
```
Noticed while working towards "Pragmatic quotients".
```
  905203e1
- well_founded.v: add Acc_dep_ind induction principle for Acc · 2df65b35
  Paolo G. Giarrusso authored Oct 01, 2021
  
  2df65b35
- well_founded.v: stop requiring tactics · 61dd9360
  Paolo G. Giarrusso authored Oct 26, 2021
  
  61dd9360
- Split well_founded.v out of relations.v · 73c7d80a
  Paolo G. Giarrusso authored Oct 26, 2021
```
No changes to the contents.
```
  73c7d80a
26 Oct, 2021 4 commits
- relations.v: Drop stale require · 0190372d
  Paolo G. Giarrusso authored Oct 26, 2021
  
  0190372d
- Merge branch 'monadset-comments' into 'master' · 0499e9bc
  Robbert Krebbers authored Oct 26, 2021
```
base.v: fix typo in comment about MonadSet, and extend

See merge request !332
```
  0499e9bc
- base.v: fix typo in comment about MonadSet, and extend · 17414dc7
  Paolo G. Giarrusso authored Oct 26, 2021 and Robbert Krebbers committed Oct 26, 2021
  
  17414dc7
- Merge branch 'finite_sets_2' into 'master' · e9aae334
  Robbert Krebbers authored Oct 26, 2021
```
Mark set_size and set_fold as TC opaque

See merge request !329
```
  e9aae334