- 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 12, 2018
-
-
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 04, 2018
-
-
Robbert Krebbers authored
-
- Nov 01, 2018
-
-
Robbert Krebbers authored
-
- Oct 04, 2018
-
-
Robbert Krebbers authored
This makes some proress on #21. Still, the question remains if a more generic solution exists.
-
- Jun 30, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 29, 2018
-
-
Janno authored
-
- Jun 28, 2018
-
-
Ralf Jung authored
-
- Jun 25, 2018
-
-
Ralf Jung authored
-
- Jun 20, 2018
-
-
Ralf Jung authored
-
- Jun 18, 2018
- Jun 14, 2018
-
-
Ralf Jung authored
-
- Jun 10, 2018
-
-
Robbert Krebbers authored
-
Ralf Jung authored
Works around Coq bug #7731
-
- Jun 09, 2018
- Jun 07, 2018
-
-
Ralf Jung authored
-
- Jun 06, 2018
- May 29, 2018
-
-
Ralf Jung authored
-
- May 28, 2018
-
-
Ralf Jung authored
-
- May 24, 2018
-
-
Ralf Jung authored
The notation was parsing-only 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`.
-
- May 23, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 14, 2018
-
-
Robbert Krebbers authored
-
- Apr 27, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Apr 21, 2018
- Apr 11, 2018
-
-
Robbert Krebbers authored
-
- Apr 09, 2018
-
-
Robbert Krebbers authored
This fixes issue #12.
-
Robbert Krebbers authored
-