- 13 Jan, 2019 1 commit
-
-
Robbert Krebbers authored
`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instance See merge request iris/stdpp!48
-
- 11 Jan, 2019 1 commit
-
-
Robbert Krebbers authored
-
- 19 Dec, 2018 1 commit
-
-
Ralf Jung authored
-
- 16 Dec, 2018 1 commit
-
-
Robbert Krebbers authored
Add results about deleting and inserting filtered out elements See merge request iris/stdpp!46
-
- 15 Dec, 2018 2 commits
-
-
Mackie Loeffel authored
-
Ralf Jung authored
Get rid of the awk.Makefile references See merge request iris/stdpp!47
-
- 14 Dec, 2018 1 commit
-
-
Dan Frumin authored
-
- 12 Dec, 2018 1 commit
-
-
Robbert Krebbers authored
Two reasons: - The equality makes it very hard to use the lemma with `rewrite`. - The version for lists `insert_zip_with` does not have the equality either.
-
- 30 Nov, 2018 5 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Add link to docs to the Readme See merge request iris/stdpp!42
-
Robbert Krebbers authored
Explicitly use core hint database See merge request iris/stdpp!43
-
- 28 Nov, 2018 1 commit
-
-
Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).
-
- 26 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 22 Nov, 2018 2 commits
-
-
Ralf Jung authored
-
Mackie Loeffel authored
-
- 20 Nov, 2018 1 commit
-
-
Ralf Jung authored
-
- 12 Nov, 2018 3 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- 11 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
- Interaction with delete - Make name about map interacting with insert consistent.
-
- 10 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 09 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 08 Nov, 2018 3 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
MR #41 relies on https://github.com/coq/coq/issues/5039, which has not been fixed in Coq 8.6.
-
Robbert Krebbers authored
Consistently block `simpl` on all `Z` operations See merge request iris/stdpp!41
-
- 04 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 01 Nov, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 15 Oct, 2018 2 commits
- 07 Oct, 2018 1 commit
-
-
Ralf Jung authored
-
- 04 Oct, 2018 2 commits
-
-
Robbert Krebbers authored
This makes some proress on #21. Still, the question remains if a more generic solution exists.
-
Ralf Jung authored
-
- 30 Sep, 2018 1 commit
-
-
Ralf Jung authored
-
- 18 Sep, 2018 5 commits