diff options
| author | Hugo Herbelin | 2014-11-22 18:16:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-22 19:10:33 +0100 |
| commit | d9681fb94a3e04a618e58cd09df9cee929170edc (patch) | |
| tree | aaba8395c5202383d7e8d17c323b10798124cd16 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions