Commits · 06da8f18662cc546a0e3c6c3d0f03f0603f2200e · Adam / stdpp

Feb 19, 2020
- test 8.11.dev instead of master · 06da8f18
  Ralf Jung authored 5 years ago
  
  06da8f18
Feb 18, 2020
- Merge branch 'robbert/top_set' into 'master' · af368a15
  Robbert Krebbers authored 5 years ago
  
  Add class `TopSet` for sets with ⊤ element Closes #49 See merge request !111
  af368a15
Feb 17, 2020
- CHANGELOG entry. · ab51e3fd
  Robbert Krebbers authored 5 years ago
  
  ab51e3fd
- `TopSet` instance for `boolset`. · 2ad56b99
  Robbert Krebbers authored 5 years ago
  
  2ad56b99
- Add class `TopSet` for sets with ⊤ element. · e09f7ce3
  Robbert Krebbers authored 5 years ago
  
  This closes issue #49.
  e09f7ce3
- Move lattice related stuff up. · ddfcc76c
  Robbert Krebbers authored 5 years ago
  
  ddfcc76c
- Remove obsolete `Hint Extern`s that predate the `Hint Mode` declarations. · 9a1b4cde
  Robbert Krebbers authored 5 years ago
  
  9a1b4cde
Feb 14, 2020
- `Prop` is inhabited. · 718ca5be
  Robbert Krebbers authored 5 years ago
  
  718ca5be
Feb 13, 2020
- Merge branch 'z-greater-decidability' into 'master' · b5a66ffb
  Robbert Krebbers authored 5 years ago
  
  Add decidability instances for Z.gt and Z.ge See merge request !110
  b5a66ffb
- Add decidability instances for Z.gt and Z.ge · 583c4645
  Tej Chajed authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  583c4645
- drop 8.9 timing again · 355c84cf
  Ralf Jung authored 5 years ago
  
  355c84cf
Feb 11, 2020
- temporarily also time 8.9.1 again · e95c967d
  Ralf Jung authored 5 years ago
  
  e95c967d
- enable docs again · 1dd79bce
  Ralf Jung authored 5 years ago
  
  1dd79bce
- rely on default timing conf name · c65f3e39
  Ralf Jung authored 5 years ago
  
  c65f3e39
- time on 8.11 instead of 8.10 · 71b46811
  Ralf Jung authored 5 years ago
  
  71b46811
- Merge branch 'lookup_total' into 'master' · 52ed0a36
  Robbert Krebbers authored 5 years ago
  
  LookupTotal See merge request !97
  52ed0a36
- Fix the notation for LookupTotal · 41c1305d
  Dan Frumin authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  In accordance with <!93>
  41c1305d
Feb 01, 2020
- test 8.11.0 release · 6caf9b6d
  Ralf Jung authored 5 years ago
  
  6caf9b6d
Jan 30, 2020
- Merge branch 'tcforall2_forall' into 'master' · 070f2235
  Robbert Krebbers authored 5 years ago
  
  Added TCForall2_Forall2 lemma See merge request !107
  070f2235
- added tcforall2_forall lemma · 81f9b193
  Michael Sammler authored 5 years ago
  
  81f9b193
Jan 18, 2020
- Add lemma `binder_delete_empty`. · 7e0096d8
  Robbert Krebbers authored 5 years ago
  
  7e0096d8
Jan 17, 2020
- Add lemma `map_lookup_zip_with_Some`. · 50efdf9c
  Robbert Krebbers authored 5 years ago
  
  50efdf9c
- Add `map_zip_with_proper`. · 9008bf44
  Robbert Krebbers authored 5 years ago
  
  9008bf44
- `Proper` instances for HO-functions on lists. · f3982420
  Robbert Krebbers authored 5 years ago
  
  Namely, `fmap`, `omap`, `imap`, `mbind`, `mjoin`, `zip_with`. As part of this, refactor slightly to put all `omap`, `imap`, and `seq` results together.
  f3982420
Jan 16, 2020
- Add lemma `lookup_zip_with_Some`. · ff383745
  Robbert Krebbers authored 5 years ago
  
  ff383745
Jan 15, 2020
- Strengten `fmap_equiv_ext` lemmas. · ec91c14f
  Robbert Krebbers authored 5 years ago
  
  The `Equiv` instance for the domain is not needed.
  ec91c14f
- Some generic results on binders that were in Iris. · 436d274d
  Robbert Krebbers authored 5 years ago
  
  436d274d
- Lemma for lookup of cons. · f4f0f216
  Robbert Krebbers authored 5 years ago
  
  f4f0f216
Jan 13, 2020
- fix README · 254512a9
  Ralf Jung authored 5 years ago
  
  254512a9
- stop timing Coq master · e0d3bf2c
  Ralf Jung authored 5 years ago
  
  e0d3bf2c
- fix opam version number · 449b53e9
  Ralf Jung authored 5 years ago
  
  449b53e9
- disable docs building for now, SSH login is broken · d322b6fd
  Ralf Jung authored 5 years ago
  
  d322b6fd
- opam 2 upgrade · df4fbcb4
  Ralf Jung authored 5 years ago
  
  df4fbcb4
Dec 19, 2019
- temporarily time Coq master · bcb89f76
  Ralf Jung authored 5 years ago
  
  bcb89f76
Dec 06, 2019
- bump to Coq 8.10.2 · 1ef53c55
  Ralf Jung authored 5 years ago
  
  1ef53c55
Nov 22, 2019
- Coq 8.11 is fixed · d2265de7
  Ralf Jung authored 5 years ago
  
  d2265de7
- allow 8.11 job to fail while we investigate · 16eb222f
  Ralf Jung authored 5 years ago
  
  16eb222f
- make opam dependency more tightly match what we test · bc360fe8
  Ralf Jung authored 5 years ago
  
  bc360fe8
- test the Coq 8.11 branch · 7ae24ef3
  Ralf Jung authored 5 years ago
  
  7ae24ef3
Nov 21, 2019
- Merge branch 'opaquify-gmap' into 'master' · 2b916512
  Robbert Krebbers authored 5 years ago
  
  Opaquify proofs in gmap_partial_alter (fix #46) Closes #46 See merge request !106
  2b916512