- May 27, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 22, 2016
-
-
Robbert Krebbers authored
Initial commit by Amin Timany.
-
Robbert Krebbers authored
-
- May 04, 2016
-
-
Janno authored
-
- Apr 29, 2016
-
-
Robbert Krebbers authored
-
- Apr 13, 2016
-
-
Robbert Krebbers authored
-
- Apr 11, 2016
-
-
Robbert Krebbers authored
-
- Apr 07, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 30, 2016
-
-
Robbert Krebbers authored
This seems to shorten type class search.
-
- Mar 29, 2016
-
-
Robbert Krebbers authored
-
- Mar 23, 2016
-
-
Ralf Jung authored -
Robbert Krebbers authored
-
- Mar 22, 2016
-
-
Ralf Jung authored
-
- Mar 21, 2016
-
-
Robbert Krebbers authored
Also, slightly reorganize.
-
Robbert Krebbers authored
-
- Mar 11, 2016
-
-
Robbert Krebbers authored
-
- Mar 10, 2016
-
-
Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.
-
- Mar 05, 2016
- Mar 04, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 03, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Contrary to destruct_conj from Program.
-
Robbert Krebbers authored
-
- Mar 02, 2016
-
-
Ralf Jung authored
-
- Feb 27, 2016
-
-
Robbert Krebbers authored
-
- Feb 26, 2016
-
-
Robbert Krebbers authored
-
- Feb 25, 2016
-
-
Ralf Jung authored
-
Robbert Krebbers authored
It now turns setoid equalities into Leibniz equalities when possible, and substitutes those.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
In principle, we could now un-seal heap_mapsto, saved_prop_own etc., and mark them as "Typeclass Opaque", and ecancel would still work just as fast as it does now. Thanks to Matthieu for pointing me to this unify feature.
-
