Commits · f4718436681da181951e4b15fc7ff1b682b4114d · Adam / stdpp

Jul 01, 2020

Fix #70: add pattern variant of bind notation · f4718436

Use that in place of the old encoding:
iris/stdpp#70 (comment 52817)

Requires dropping support for Coq 8.7.

Verified

f4718436

Jun 29, 2020
- Merge branch 'robbert/multiset_solver' into 'master' · 376e5e05
  Robbert Krebbers authored 4 years ago
  
  Add solver `multiset_solver` for multisets See merge request !167
  376e5e05
Jun 25, 2020
- Make `multiset_solver` stronger by also considering `multiplicity` in hyps. · 45b64e21
  Robbert Krebbers authored 4 years ago
  
  45b64e21
- CHANGELOG. · f4269240
  Robbert Krebbers authored 4 years ago
  
  f4269240
- Add tests for `multiset_solver`. · 8f80353d
  Robbert Krebbers authored 4 years ago
  
  8f80353d
- Add solver `multiset_solver` for multisets. · d3d95ed9
  Robbert Krebbers authored 4 years ago
  
  d3d95ed9
- Export `Countable` in `gmultiset`, without that, the file is useless. · fd6905fa
  Robbert Krebbers authored 4 years ago
  
  fd6905fa
Jun 23, 2020
- Merge branch 'gset-gmap-delete' into 'master' · 6ee0e09e
  Robbert Krebbers authored 4 years ago
  
  Prove theorem about delete of gset_to_gmap See merge request !162
  6ee0e09e
Jun 19, 2020
- bump Coq to 8.11.2 · aa5e294c
  Ralf Jung authored 4 years ago
  
  aa5e294c
- update Makefile · 4e96f9ee
  Ralf Jung authored 4 years ago
  
  4e96f9ee
Jun 18, 2020
- Merge branch 'master' into 'master' · 99bad668
  Robbert Krebbers authored 4 years ago
  
  Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) See merge request !164
  99bad668
- Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) · 3dce1fea
  sarahzrf authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  3dce1fea
Jun 17, 2020
- Fix compatibility with old Coq versions. · 370c0cf4
  Robbert Krebbers authored 4 years ago
  
  370c0cf4
- Merge branch 'robbert/coq_12512' into 'master' · 2f5854bd
  Robbert Krebbers authored 4 years ago
  
  Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512 See merge request !166
  2f5854bd
Jun 15, 2020
- Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512. · 6af69af1
  Robbert Krebbers authored 4 years ago
  
  6af69af1
- Turn some non-recursive `Fixpoint`s into `Definition`s. · 2ec23bde
  Robbert Krebbers authored 4 years ago
  
  2ec23bde
Jun 14, 2020
- Fix inconsistent space. · 6401d876
  Robbert Krebbers authored 4 years ago
  
  6401d876
May 29, 2020
- Coq 8.11.2 tag exists but there is no such release · 9bd10869
  Ralf Jung authored 4 years ago
  
  9bd10869
- test Coq 8.11.2, and the Coq 8.12 branch · 73e64b7a
  Ralf Jung authored 4 years ago
  
  73e64b7a
- permit building with Coq 8.12 · b6d4c71e
  Ralf Jung authored 4 years ago
  
  b6d4c71e
May 27, 2020
- Merge branch 'fix-forall-scope' into 'master' · 3196e5ca
  Robbert Krebbers authored 4 years ago
  
  Remove type scope from forall notation Closes #67 See merge request !163
  3196e5ca
- Remove type scope from forall notation · b36cd736
  Tej Chajed authored 4 years ago
  
  Fixes #67.
  Verified
  
  b36cd736
- Merge branch 'forall-notation' into 'master' · 60ad150d
  Robbert Krebbers authored 4 years ago
  
  notation for forall See merge request !152
  60ad150d
- notation for forall · bfb8f04e
  Gregory Malecha authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  bfb8f04e
May 26, 2020
- Prove theorem about delete of gset_to_gmap · a04b0a88
  Tej Chajed authored 4 years ago
  
  Verified
  
  a04b0a88
May 12, 2020
- Merge branch 'msammler/rename_Nat2Z_inj_div' into 'master' · ea934fb9
  Robbert Krebbers authored 4 years ago
  
  rename Z2Nat_inj_div and Z2Nat_inj_mod See merge request iris/stdpp!161
  ea934fb9
- rename Z2Nat_inj_div and Z2Nat_inj_mod · 0eaae21d
  Michael Sammler authored 4 years ago
  
  0eaae21d
- Merge branch 'revert-a2ac9e66 ' into 'master' · fd5ab7ff
  Robbert Krebbers authored 4 years ago
  
  Revert "Merge branch 'byte-countable' into 'master'" See merge request iris/stdpp!160
  fd5ab7ff
- Revert "Merge branch 'byte-countable' into 'master'" · e99804d9
  Robbert Krebbers authored 4 years ago
  
  This reverts merge request !155
  e99804d9
- Merge branch 'byte-countable' into 'master' · a2ac9e66
  Robbert Krebbers authored 4 years ago
  
  Add Countable instances for byte See merge request iris/stdpp!155
  a2ac9e66
- Add Countable instances for byte · 5346dd70
  Tej Chajed authored 4 years ago
  
  Verified
  
  5346dd70
- Merge branch 'robbert/list_find' into 'master' · befe38d4
  Robbert Krebbers authored 4 years ago
  
  Lemmas for `list_find` in combination with `app` and `insert`. See merge request iris/stdpp!134
  befe38d4
- CHANGELOG entry. · e6b17ca4
  Robbert Krebbers authored 4 years ago
  
  e6b17ca4
- Lemmas for `list_find` in combination with `app` and `insert`. · 4680e914
  Robbert Krebbers authored 4 years ago
  
  4680e914
- Make `list_find_Some` more `apply` friendly. · 278a845b
  Robbert Krebbers authored 4 years ago
  
  278a845b
- Merge branch 'msammler/rotate' into 'master' · 199c984b
  Robbert Krebbers authored 4 years ago
  
  Rotate everything See merge request iris/stdpp!136
  199c984b
- Added rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions · a613b693
  Michael Sammler authored 4 years ago
  
  a613b693
May 07, 2020
- Merge branch 'ralf/map-forall-lookup' into 'master' · fb90d2d8
  Robbert Krebbers authored 4 years ago
  
  add map_Forall_lookup See merge request iris/stdpp!158
  fb90d2d8
- prove lemma in both directions · a6d4d077
  Ralf Jung authored 4 years ago
  
  a6d4d077
- Merge branch 'bool-leb2' into 'master' · 56a8ce93
  Robbert Krebbers authored 4 years ago
  
  alternative overlay for coq/coq#12162 See merge request iris/stdpp!159
  56a8ce93