- Jul 19, 2016
- Jul 16, 2016
-
-
Robbert Krebbers authored
This reverts commit 6076bbc6.
-
- Jul 15, 2016
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Jul 13, 2016
-
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
The intropattern {H} also meant clear (both in ssreflect, and the logic part of the introduction pattern).
-
Ralf Jung authored
-
- Jul 12, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 11, 2016
-
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This class whose name is horrible and purpose is arbitrary seems to be a leftover of some experiment with ch2o, a long time a ago.
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jul 06, 2016
-
-
Jacques-Henri Jourdan authored
-
- Jul 05, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 04, 2016
-
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
- Jul 03, 2016
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
That way type class search becomes more predictable.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-