- 19 Jul, 2016 2 commits
- 18 Jul, 2016 4 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 16 Jul, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 15 Jul, 2016 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 13 Jul, 2016 5 commits
-
-
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
-
- 12 Jul, 2016 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 11 Jul, 2016 7 commits
-
-
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
-
- 06 Jul, 2016 1 commit
-
-
Jacques-Henri Jourdan authored
-
- 05 Jul, 2016 7 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 04 Jul, 2016 2 commits
-
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
- 03 Jul, 2016 6 commits
-
-
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
-