- Jan 24, 2019
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
fix λ.. printing and test it See merge request iris/stdpp!51
-
Ralf Jung authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Make trivial instances explicit See merge request !50
-
- Jan 23, 2019
-
-
Maxime Dénès authored
This is in preparation for coq/coq#9274.
-
- Jan 13, 2019
-
-
Robbert Krebbers authored
`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instance See merge request !48
-
- Jan 11, 2019
-
-
Robbert Krebbers authored
-
- Dec 19, 2018
-
-
Ralf Jung authored
-
- Dec 16, 2018
-
-
Robbert Krebbers authored
Add results about deleting and inserting filtered out elements See merge request !46
-
- Dec 15, 2018
-
-
Mackie Loeffel authored
-
- Dec 14, 2018
-
-
Dan Frumin authored
-
- Dec 12, 2018
-
-
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.
-
- Nov 30, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Explicitly use core hint database See merge request !43
-
- Nov 28, 2018
-
-
Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).
-
- Nov 26, 2018
-
-
Robbert Krebbers authored
-
- Nov 22, 2018
-
-
Ralf Jung authored
-
Mackie Loeffel authored
-
- Nov 20, 2018
-
-
Ralf Jung authored
-
- Nov 12, 2018
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Nov 11, 2018
-
-
Robbert Krebbers authored
- Interaction with delete - Make name about map interacting with insert consistent.
-
- Nov 10, 2018
-
-
Robbert Krebbers authored
-
- Nov 09, 2018
-
-
Robbert Krebbers authored
-
- Nov 08, 2018
-
-
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 !41
-
- Nov 04, 2018
-
-
Robbert Krebbers authored
-
- Nov 01, 2018
-
-
Robbert Krebbers authored
-
- Oct 15, 2018
-
-
Ralf Jung authored
-