Commits · af368a15906653d7b607724aedd28ced4152ab0e · Iris / stdpp

18 Feb, 2020 1 commit
- Merge branch 'robbert/top_set' into 'master' · af368a15
  Robbert authored Feb 18, 2020
```
Add class `TopSet` for sets with ⊤ element

Closes #49

See merge request !111
```
  af368a15
17 Feb, 2020 5 commits
- CHANGELOG entry. · ab51e3fd
  Robbert Krebbers authored Feb 17, 2020
  
  ab51e3fd
- `TopSet` instance for `boolset`. · 2ad56b99
  Robbert Krebbers authored Feb 17, 2020
  
  2ad56b99
- Add class `TopSet` for sets with ⊤ element. · e09f7ce3
  Robbert Krebbers authored Feb 17, 2020
```
This closes issue #49.
```
  e09f7ce3
- Move lattice related stuff up. · ddfcc76c
  Robbert Krebbers authored Feb 17, 2020
  
  ddfcc76c
- Remove obsolete `Hint Extern`s that predate the `Hint Mode` declarations. · 9a1b4cde
  Robbert Krebbers authored Feb 17, 2020
  
  9a1b4cde
14 Feb, 2020 1 commit
- `Prop` is inhabited. · 718ca5be
  Robbert Krebbers authored Feb 14, 2020
  
  718ca5be
13 Feb, 2020 3 commits
- Merge branch 'z-greater-decidability' into 'master' · b5a66ffb
  Robbert authored Feb 13, 2020
```
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 Feb 13, 2020
  
  583c4645
- drop 8.9 timing again · 355c84cf
  Ralf Jung authored Feb 13, 2020
  
  355c84cf
11 Feb, 2020 6 commits
- temporarily also time 8.9.1 again · e95c967d
  Ralf Jung authored Feb 11, 2020
  
  e95c967d
- enable docs again · 1dd79bce
  Ralf Jung authored Feb 11, 2020
  
  1dd79bce
- rely on default timing conf name · c65f3e39
  Ralf Jung authored Feb 11, 2020
  
  c65f3e39
- time on 8.11 instead of 8.10 · 71b46811
  Ralf Jung authored Feb 11, 2020
  
  71b46811
- Merge branch 'lookup_total' into 'master' · 52ed0a36
  Robbert authored Feb 11, 2020
```
LookupTotal

See merge request !97
```
  52ed0a36
- Fix the notation for LookupTotal · 41c1305d
  Dan Frumin authored Feb 11, 2020
```
In accordance with
<!93>
```
  41c1305d
01 Feb, 2020 1 commit
- test 8.11.0 release · 6caf9b6d
  Ralf Jung authored Feb 01, 2020
  
  6caf9b6d
30 Jan, 2020 2 commits
- Merge branch 'tcforall2_forall' into 'master' · 070f2235
  Robbert authored Jan 30, 2020
```
Added TCForall2_Forall2 lemma

See merge request !107
```
  070f2235
- added tcforall2_forall lemma · 81f9b193
  Michael Sammler authored Jan 30, 2020
  
  81f9b193
18 Jan, 2020 1 commit
- Add lemma `binder_delete_empty`. · 7e0096d8
  Robbert Krebbers authored Jan 18, 2020
  
  7e0096d8
17 Jan, 2020 3 commits
- Add lemma `map_lookup_zip_with_Some`. · 50efdf9c
  Robbert Krebbers authored Jan 16, 2020
  
  50efdf9c
- Add `map_zip_with_proper`. · 9008bf44
  Robbert Krebbers authored Jan 16, 2020
  
  9008bf44
- `Proper` instances for HO-functions on lists. · f3982420
  Robbert Krebbers authored Jan 16, 2020
```
Namely, `fmap`, `omap`, `imap`, `mbind`, `mjoin`, `zip_with`.

As part of this, refactor slightly to put all `omap`, `imap`, and `seq`
results together.
```
  f3982420
16 Jan, 2020 1 commit
- Add lemma `lookup_zip_with_Some`. · ff383745
  Robbert Krebbers authored Jan 16, 2020
  
  ff383745
15 Jan, 2020 3 commits
- Strengten `fmap_equiv_ext` lemmas. · ec91c14f
  Robbert Krebbers authored Jan 15, 2020
```
The `Equiv` instance for the domain is not needed.
```
  ec91c14f
- Some generic results on binders that were in Iris. · 436d274d
  Robbert Krebbers authored Jan 15, 2020
  
  436d274d
- Lemma for lookup of cons. · f4f0f216
  Robbert Krebbers authored Jan 15, 2020
  
  f4f0f216
13 Jan, 2020 5 commits
- fix README · 254512a9
  Ralf Jung authored Jan 13, 2020
  
  254512a9
- stop timing Coq master · e0d3bf2c
  Ralf Jung authored Jan 13, 2020
  
  e0d3bf2c
- fix opam version number · 449b53e9
  Ralf Jung authored Jan 13, 2020
  
  449b53e9
- disable docs building for now, SSH login is broken · d322b6fd
  Ralf Jung authored Jan 13, 2020
  
  d322b6fd
- opam 2 upgrade · df4fbcb4
  Ralf Jung authored Jan 13, 2020
  
  df4fbcb4
19 Dec, 2019 1 commit
- temporarily time Coq master · bcb89f76
  Ralf Jung authored Dec 19, 2019
  
  bcb89f76
06 Dec, 2019 1 commit
- bump to Coq 8.10.2 · 1ef53c55
  Ralf Jung authored Dec 06, 2019
  
  1ef53c55
22 Nov, 2019 4 commits
- Coq 8.11 is fixed · d2265de7
  Ralf Jung authored Nov 22, 2019
  
  d2265de7
- allow 8.11 job to fail while we investigate · 16eb222f
  Ralf Jung authored Nov 22, 2019
  
  16eb222f
- make opam dependency more tightly match what we test · bc360fe8
  Ralf Jung authored Nov 22, 2019
  
  bc360fe8
- test the Coq 8.11 branch · 7ae24ef3
  Ralf Jung authored Nov 22, 2019
  
  7ae24ef3
21 Nov, 2019 2 commits
- Merge branch 'opaquify-gmap' into 'master' · 2b916512
  Robbert authored Nov 21, 2019
```
Opaquify proofs in gmap_partial_alter (fix #46)

Closes #46

See merge request !106
```
  2b916512
- Opaquify proofs in gmap_partial_alter (fix #46) · f7382c32
  Paolo G. Giarrusso authored Nov 21, 2019
```
- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.
```
  f7382c32