diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-22 18:16:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 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