diff options
author | 2014-11-22 18:16:05 +0100 | |
---|---|---|
committer | 2014-11-22 19:10:33 +0100 | |
commit | d9681fb94a3e04a618e58cd09df9cee929170edc (patch) | |
tree | aaba8395c5202383d7e8d17c323b10798124cd16 /test-suite/kernel | |
parent | 67b605dee0e6baee10e31805409d8a33ff71e43a (diff) |
Removing a hack which, according to the comment, should not be necessary
anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
Diffstat (limited to 'test-suite/kernel')
0 files changed, 0 insertions, 0 deletions