 11 Jan, 2019 1 commit


Robbert Krebbers authored

 15 Dec, 2018 1 commit


Mackie Loeffel 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 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 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

 12 Nov, 2018 1 commit


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

 04 Nov, 2018 1 commit


Robbert Krebbers authored

 01 Nov, 2018 1 commit


Robbert Krebbers authored

 04 Oct, 2018 1 commit


Robbert Krebbers authored
This makes some proress on #21. Still, the question remains if a more generic solution exists.

 30 Jun, 2018 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 29 Jun, 2018 1 commit


Janno authored

 28 Jun, 2018 1 commit


Ralf Jung authored

 25 Jun, 2018 1 commit


Ralf Jung authored

 20 Jun, 2018 1 commit


Ralf Jung authored

 18 Jun, 2018 2 commits
 14 Jun, 2018 1 commit


Ralf Jung authored

 10 Jun, 2018 2 commits


Robbert Krebbers authored

Ralf Jung authored
Works around Coq bug #7731

 09 Jun, 2018 3 commits
 07 Jun, 2018 1 commit


Ralf Jung authored

 06 Jun, 2018 3 commits
 29 May, 2018 1 commit


Ralf Jung authored

 28 May, 2018 1 commit


Ralf Jung authored

 24 May, 2018 1 commit


Ralf Jung authored
The notation was parsingonly and all it did was reorder the arguments for from_option. This creates just a needless divergence between what is written and what is printed. Also, removing it frees the name for maybe introducing a function or notation `default` with a type like `T > option T > T`.

 23 May, 2018 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 14 May, 2018 1 commit


Robbert Krebbers authored

 27 Apr, 2018 1 commit


Robbert Krebbers authored
