Commits · master · David Swasey / coq-stdpp

Feb 20, 2020
- Merge branch 'cogset' into 'master' · 74649a4b
  Robbert Krebbers authored 5 years ago
  74649a4b
Feb 19, 2020
- Add `coGset`. · f5abe554
  David Swasey authored 5 years ago
  
  f5abe554
- Add lemma `not_elem_of_iff`. · 157ae750
  David Swasey authored 5 years ago
  
  157ae750
- Fix compilation after !112 broke it. · e0eef94a
  Robbert Krebbers authored 5 years ago
  
  e0eef94a
- Merge branch 'ralf/hints' into 'master' · f84c69f6
  Robbert Krebbers authored 5 years ago
  f84c69f6
- add comment · 829dc991
  Ralf Jung authored 5 years ago
  
  829dc991
- move coPset-generic hint to coPset.v · a5ee0c16
  Ralf Jung authored 5 years ago
  
  a5ee0c16
- Put `top_subseteq` in core DB to fix Iris regression. · 1f223f8f
  Robbert Krebbers authored 5 years ago
  
  1f223f8f
- 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
  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
  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
  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
  52ed0a36
- Fix the notation for LookupTotal · 41c1305d
  Dan Frumin authored 5 years ago and Robbert Krebbers committed 5 years ago
  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
  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
  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
  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